mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

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

Tactic:
refine le_trans ?_ (agmSequences_fst_le_agm 0)

Goal state after:
x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ x ≤ (x.agmSequences y 0).1
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
⊢ min x y < x.agm y

Tactic:
wlog h : x < y generalizing x y
  · simpa [agm_comm, min_comm] using this hy hx hn.symm (hn.gt_or_lt.resolve_right h)
  rw [min_eq_left h.le]
  refine lt_of_le_of_lt ?_ (agmSequences_fst_lt_agm_of_pos_of_ne hx hy hn 0)
  rw [agmSequences_zero]
  exact (le_gm_and_am_le h.le).1

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
s : Set A := {a | IsStrictlyPositive a}
f : ℝ → A → A := fun p a ↦ if a ∈ s then cfc (fun x ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : A → A := fun a ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
h_convex : Convex ℝ s
⊢ ConcaveOn ℝ s fun a ↦ a ^ p - 1

Tactic:
refine ConcaveOn.sub ?_ (convexOn_const _ h_convex)

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
s : Set A := {a | IsStrictlyPositive a}
f : ℝ → A → A := fun p a ↦ if a ∈ s then cfc (fun x ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : A → A := fun a ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
h_convex : Convex ℝ s
⊢ ConcaveOn ℝ s fun a ↦ a ^ p
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
this : log (b / a) • V = ∫ (x : ℝ) in a..b, x⁻¹ • V
⊢ (∫ (x : ℝ) in a..b, x⁻¹ • f x) - ∫ (x : ℝ) in a..b, x⁻¹ • V = ∫ (x : ℝ) in a..b, x⁻¹ • (f x - V)

Tactic:
← integral_sub hint_f hint_V

Goal state after:
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 : ℝ) in a..b, x⁻¹ • f x - x⁻¹ • V = ∫ (x : ℝ) in a..b, x⁻¹ • (f x - V)
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
hsplit :
  ∀ {ε r : ℝ},
    0 < ε →
      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
ε r : ℝ
⊢ (ε, r) ∈ {x | x ∈ Ioi 0} ×ˢ {x | 0 < x} →
    ∫ (x : ℝ) in (ε, r).1..(ε, r).2, x⁻¹ • (f (a * x) - f (b * x)) =
      (∫ (x : ℝ) in a * (ε, r).1..b * (ε, r).1, u x) - ∫ (x : ℝ) in a * (ε, r).2..b * (ε, r).2, u x

Tactic:
⟨hε, hr⟩

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
hsplit :
  ∀ {ε r : ℝ},
    0 < ε →
      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
ε r : ℝ
hε : (ε, r).1 ∈ {x | x ∈ Ioi 0}
hr : (ε, r).2 ∈ {x | 0 < x}
⊢ ∫ (x : ℝ) in (ε, r).1..(ε, r).2, x⁻¹ • (f (a * x) - f (b * x)) =
    (∫ (x : ℝ) in a * (ε, r).1..b * (ε, r).1, u x) - ∫ (x : ℝ) in a * (ε, r).2..b * (ε, r).2, u x
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case refine_1.refine_1
p : ℝ
hp : p ∈ Ioo 0 1
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun q ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
⊢ ContinuousOn (fun q ↦ q.1 ^ (p - 1) * q.2) (Ioi 0 ×ˢ s)

Tactic:
refine ContinuousOn.mul ?_ (by fun_prop)

Goal state after:
case refine_1.refine_1
p : ℝ
hp : p ∈ Ioo 0 1
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun q ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
⊢ ContinuousOn (fun q ↦ q.1 ^ (p - 1)) (Ioi 0 ×ˢ s)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case neg
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)

Tactic:
case neg =>
    calc
    _ = t ^ (p - 1) * x / (t + x) := by rw [rpowIntegrand₀₁_eq_pow_div hp ht hx]
    _ ≤ t ^ (p - 1) * x / x := by gcongr; linarith
    _ = t ^ (p - 1) * (x / x) := by ring
    _ = t ^ (p - 1) * 1 := by congr; exact (div_eq_one_iff_eq hx_zero).mpr rfl
    _ = _ := by simp

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

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

Tactic:
refine ae_restrict_of_forall_mem measurableSet_Ioi fun t (ht : 1 < t) => ?_

Goal state after:
p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
t : ℝ
ht : 1 < t
⊢ ‖p.rpowIntegrand₀₁ t x‖ ≤ t ^ (p - 2) * x
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp 1 ^ (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ rexp (107 / 60) < 6

Tactic:
exp_one_rpow

Goal state after:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ rexp (107 / 60) < 6
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
h2 : 0 < (↑π / a).re
f_bd : f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
x : ℝ
⊢ -(↑π * a⁻¹ * ↑x * I * b * 2) - ↑π * a⁻¹ * ↑x ^ 2 - ↑π * a⁻¹ * I ^ 2 * b ^ 2 =
    -(↑π * a⁻¹ * ↑x * I * b * 2) - ↑π * a⁻¹ * ↑x ^ 2 + ↑π * a⁻¹ * b ^ 2

Tactic:
rw [I_sq]

Goal state after:
a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
h2 : 0 < (↑π / a).re
f_bd : f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
x : ℝ
⊢ -(↑π * a⁻¹ * ↑x * I * b * 2) - ↑π * a⁻¹ * ↑x ^ 2 - ↑π * a⁻¹ * -1 * b ^ 2 =
    -(↑π * a⁻¹ * ↑x * I * b * 2) - ↑π * a⁻¹ * ↑x ^ 2 + ↑π * a⁻¹ * b ^ 2
Module: Mathlib.Data.Int.Log

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

Tactic:
rw [log_of_one_le_right _ hr1, Int.ofNat_add_one_out]

Goal state after:
case inr.inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : 1 ≤ r
⊢ r < ↑b ^ ↑(Nat.log b ⌊r⌋₊).succ
Module: Mathlib.Data.Int.Log

Goal state before:
pp: R : Type u_1
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
r : R
⊢ log 1 r = 0

Tactic:
by_cases hr : 1 ≤ r

Goal state after:
case pos
R : Type u_1
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
r : R
hr : 1 ≤ r
⊢ log 1 r = 0

case neg
R : Type u_1
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
r : R
hr : ¬1 ≤ r
⊢ log 1 r = 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b : ℝ
⊢ logb b 0 = 0

Tactic:
by simp [logb]

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

Goal state before:
pp: b : ℝ
⊢ logb b 1 = 0

Tactic:
by simp [logb]

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₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
⊢ log b r₁ ≤ log b r₂

Tactic:
rcases le_total r₁ 1 with h₁ | h₁ <;> rcases le_total r₂ 1 with h₂ | h₂
  · have h₀' : 0 < r₂ := lt_of_lt_of_le h₀ h
    rw [log_of_right_le_one _ h₁, log_of_right_le_one _ h₂, neg_le_neg_iff, Nat.cast_le]
    exact Nat.clog_mono_right b <| Nat.ceil_mono <| (inv_le_inv₀ h₀' h₀).2 h
  · rw [log_of_right_le_one _ h₁, log_of_one_le_right _ h₂]
    exact (neg_nonpos.mpr (Int.natCast_nonneg _)).trans (Int.natCast_nonneg _)
  · obtain rfl := le_antisymm h (h₂.trans h₁)
    rfl
  · rw [log_of_one_le_right _ h₁, log_of_one_le_right _ h₂, Nat.cast_le]
    exact Nat.log_mono_right (Nat.floor_mono h)

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

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

Tactic:
exact log_lt_log_iff hx hy

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

Goal state before:
pp: R : Type u_1
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
r : R
⊢ clog 0 r = 0

Tactic:
by_cases hr : 1 ≤ r

Goal state after:
case pos
R : Type u_1
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
r : R
hr : 1 ≤ r
⊢ clog 0 r = 0

case neg
R : Type u_1
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
r : R
hr : ¬1 ≤ r
⊢ clog 0 r = 0
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
⊢ t ^ (p - 1) • cfcₙ (p.rpowIntegrand₀₁ 1) (t⁻¹ • b) = cfcₙ (p.rpowIntegrand₀₁ t) b

Tactic:
by
      rw [cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one hp ht b hb]

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

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

Tactic:
by
  rw [logb, logb, div_lt_div_right_of_neg (log_neg b_pos b_lt_one)]
  exact log_lt_log hx hxy

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

Goal state before:
pp: case succ
n : ℕ
ih : MonotoneOn (deriv fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) (Set.Ioi (↑n - 1))
a : ℝ
ha : ↑n + 1 - 1 < a
b : ℝ
hb : ↑n + 1 - 1 < b
hab : a ≤ b
⊢ deriv (fun x ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) a ≤
    deriv (fun x ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) b

Tactic:
add_sub_cancel_right

Goal state after:
case succ
n : ℕ
ih : MonotoneOn (deriv fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) (Set.Ioi (↑n - 1))
a : ℝ
ha : ↑n < a
b : ℝ
hb : ↑n < b
hab : a ≤ b
⊢ deriv (fun x ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) a ≤
    deriv (fun x ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) b
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

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

Tactic:
rw [← (integral_sub (integrable_mulExpNegMulSq_comp_restrict_of_isCompact hK hKmeas g)
      (integrable_mulExpNegMulSq_comp_restrict_of_isCompact hK hKmeas f)), ← norm_eq_abs]

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

Goal state before:
pp: case pos
E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < ↑(Module.finrank ℝ E)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
hr : 0 < r
⊢ IntegrableOn (fun y ↦ y ^ (↑(Module.finrank ℝ E) - 1 - α)) (Ioo 0 r) volume

Tactic:
rw [intervalIntegral.integrableOn_Ioo_rpow_iff hr]
        linarith

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

Goal state before:
pp: guess fuel : ℕ
hle : guess ≤ fuel
n a : ℕ
⊢ go n a fuel guess ^ (n + 2) ≤ a

Tactic:
by
  induction fuel generalizing guess with
  | zero =>
    obtain rfl : guess = 0 := by grind
    simp [go]
  | succ fuel ih =>
    rw [go]
    split_ifs with h
    case pos =>
      grind
    case neg =>
      have : guess ≤ a / guess ^ (n + 1) := by
        linarith only [Nat.mul_le_of_le_div _ _ _ (not_lt.1 h)]
      replace := Nat.mul_le_of_le_div _ _ _ this
      grind

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

Goal state before:
pp: a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
this : Tendsto (fun x ↦ (1 / ↑x) ^ (b.card + 1 - a.card)) atTop (𝓝 0)
n : ℕ
⊢ (1 / ↑n) ^ (b.card + 1 - a.card) = ↑n ^ (↑a.card - ↑b.card - 1)

Tactic:
rw [one_div, inv_pow, ← zpow_natCast, ← zpow_neg, Int.ofNat_sub (by grind),
        Int.natCast_add_one]

Goal state after:
a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
this : Tendsto (fun x ↦ (1 / ↑x) ^ (b.card + 1 - a.card)) atTop (𝓝 0)
n : ℕ
⊢ ↑n ^ (-(↑b.card + 1 - ↑a.card)) = ↑n ^ (↑a.card - ↑b.card - 1)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case inr
L : PeriodPair
z : ℂ
l : ↥L.lattice
G : AddSubgroup ℂ := { carrier := {z | (fun x ↦ ℘[L] (x + z)) = ℘[L]}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
i : ℂ
⊢ ℘[L] (i + L.ω₂) = ℘[L] i

Tactic:
exact L.weierstrassP_add_coe_aux _ ⟨_, L.ω₂_mem_lattice⟩ L.ω₂_div_two_notMem_lattice

Goal state after:
Module: Mathlib.NumberTheory.Niven

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

Tactic:
by
  rw [cos.eq_1, mul_div_cancel₀ _ two_ne_zero]
  exact (isIntegral_exp_rat_mul_pi_mul_I q).add (isIntegral_exp_neg_rat_mul_pi_mul_I q)

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
n : ℕ
⊢ Disjoint (box (n + 1)) (Icc (-↑n) ↑n)

Tactic:
by
  rw [box_succ_eq_sdiff]; exact disjoint_sdiff_self_left

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

Goal state before:
pp: z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ r { coe := { re := A, im := B }, coe_im_pos := h } ≤ r z

Tactic:
apply min_le_min hz.2
  gcongr
  simp only [r1_eq, div_pow, one_div]
  rw [inv_le_inv₀ (by positivity) (by positivity), add_le_add_iff_right, ← even_two.pow_abs]
  gcongr
  exacts [hz.1, hz.2]

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

Goal state before:
pp: n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ (-1) ^ i * iterateDerivativeC n k x i

Tactic:
iterateDerivativeC,

Goal state after:
n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤
    (-1) ^ i *
      (↑k.factorial * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ *
        ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 < (-1) ^ i * iterateDerivativeC n k x i

Tactic:
iterateDerivativeC,

Goal state after:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 <
    (-1) ^ i *
      (↑k.factorial * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ *
        ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℤ
x : ℝ
hx : 1 ≤ |x|
⊢ 1 ≤ |eval x (T ℝ n)|

Tactic:
wlog! h : 0 ≤ x
  · simpa [T_eval_neg, abs_mul, abs_unit_intCast] using @this n (-x) (by grind) (by grind)
  · exact one_le_eval_T_real n (abs_of_nonneg h ▸ hx) |>.trans <| le_abs_self _

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

Goal state before:
pp: case hΘ
d : ℤ
z : ℂ
hz : z ≠ 0
⊢ (fun c ↦ ↑c * z) =Θ[cofinite] fun n ↦ ↑n

Tactic:
simp_rw [mul_comm]
    apply Asymptotics.IsTheta.const_mul_left hz Int.cast_complex_isTheta_cast_real

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : CompleteSpace F
inst✝¹ : TopologicalSpace β
inst✝ : LocallyCompactSpace β
f : α → β → F
s : Set β
hs : IsOpen[inst✝¹] s
hu : ∀ K ⊆ s, IsCompact K → ∃ u, Summable u ∧ ∀ (n : α), ∀ k ∈ K, ‖f n k‖ ≤ u n
⊢ SummableLocallyUniformlyOn f s

Tactic:
by
  apply SummableLocallyUniformlyOn.of_locally_bounded_eventually hs
  intro K hK hKc
  obtain ⟨u, hu1, hu2⟩ := hu K hK hKc
  exact ⟨u, hu1, by filter_upwards using hu2⟩

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

Goal state before:
pp: x : ℂ
h0 : x ≠ 0
n : ℕ
⊢ (↑π * x * ∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2)) * (1 / (↑π * x)) =
    ∏ i ∈ Finset.range n, (1 + sineTerm x i)

Tactic:
by field_simp; rfl

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

Goal state before:
pp: m : ℕ
n : ℤ
⊢ fib (↑(m + 2) + n) = fib (↑m + n) + fib (↑m + n + 1)

Tactic:
by grind [fib_add_two]

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

Goal state before:
pp: m : ℕ
n : ℤ
⊢ fib (↑m - 1) * fib n + fib ↑m * fib (n + 1) + fib ↑m * fib n + fib (↑m + 1) * fib (n + 1) =
    fib (↑(m + 2) - 1) * fib n + fib ↑(m + 2) * fib (n + 1)

Tactic:
by grind [fib_add_two]

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

Goal state before:
pp: n : ℤ
m : ℕ
⊢ fib (n + ↑(m + 2)) = fib (↑m + n) + fib (↑m + n + 1)

Tactic:
by grind [fib_add_two]

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

Goal state before:
pp: n : ℤ
m : ℕ
⊢ fib (↑m - 1) * fib n + fib ↑m * fib (n + 1) + fib ↑m * fib n + fib (↑m + 1) * fib (n + 1) =
    fib (n - 1) * fib ↑(m + 2) + fib n * fib (↑(m + 2) + 1)

Tactic:
by grind [fib_add_two]

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

Goal state before:
pp: m n : ℕ
⊢ fib (-↑m + -↑(n + 2)) = fib (-↑m + -↑n) - fib (-↑m + -↑(n + 1))

Tactic:
by grind [fib_add_two]

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

Goal state before:
pp: m n : ℕ
⊢ fib (-↑m - 1) * fib (-↑n) + fib (-↑m) * fib (-↑n + 1) - fib (-↑m - 1) * fib (-↑n - 1) - fib (-↑m) * fib (-↑n) =
    fib (-↑m - 1) * fib (-↑(n + 2)) + fib (-↑m) * fib (-↑(n + 2) + 1)

Tactic:
by grind [fib_add_two]

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

Goal state before:
pp: k d : ℕ
⊢ EqOn (iteratedDeriv k fun z ↦ cotTerm z d)
    (fun z ↦ (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))) (range Int.cast)ᶜ

Tactic:
exact eqOn_iteratedDeriv_cotTerm ..

Goal state after:
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime k
h : MinFacHelper n k
⊢ MinFacHelper n k'

Tactic:
by
  refine minFacHelper_1 e h fun h2 ↦ ?_
  rw [← h2] at nk
  exact nk <| minFac_prime h.one_lt.ne'

Goal state after:
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
⊢ ∫ (x : ℝ) in 0..M, x ^ k * rexp (-(c * x)) ≤ ↑k ! / c ^ (k + 1)

Tactic:
have hk : (0 : ℝ) < ↑k + 1 := by positivity

Goal state after:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < ↑k + 1
⊢ ∫ (x : ℝ) in 0..M, x ^ k * rexp (-(c * x)) ≤ ↑k ! / c ^ (k + 1)
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: case hf
k M : ℕ
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Icc ↑0 ↑M
y : ℝ
hy : y ∈ Icc ↑0 ↑M
hxy : x ≤ y
⊢ (fun x ↦ x ^ k) x ≤ (fun x ↦ x ^ k) y

Tactic:
apply pow_le_pow_left₀ (by simpa using hx.1) hxy

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

Goal state after:
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
T : VonNeumannAlgebra H
carrier✝ : Set (H →L[ℂ] H)
mul_mem'✝ : ∀ {a b : H →L[ℂ] H}, a ∈ carrier✝ → b ∈ carrier✝ → a * b ∈ carrier✝
one_mem'✝ : 1 ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝ }.carrier
add_mem'✝ :
  ∀ {a b : H →L[ℂ] H},
    a ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier →
      b ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier →
        a + b ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier
zero_mem'✝ : 0 ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier
algebraMap_mem'✝ :
  ∀ (r : ℂ),
    (algebraMap ℂ (H →L[ℂ] H)) r ∈
      { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝,
          zero_mem' := zero_mem'✝ }.carrier
star_mem'✝ :
  ∀ {a : H →L[ℂ] H},
    a ∈
        { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝,
            zero_mem' := zero_mem'✝, algebraMap_mem' := algebraMap_mem'✝ }.carrier →
      star a ∈
        { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝,
            zero_mem' := zero_mem'✝, algebraMap_mem' := algebraMap_mem'✝ }.carrier
centralizer_centralizer'✝ :
  { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝,
            algebraMap_mem' := algebraMap_mem'✝, star_mem' := star_mem'✝ }.carrier.centralizer.centralizer =
    { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝,
        algebraMap_mem' := algebraMap_mem'✝, star_mem' := star_mem'✝ }.carrier
h :
  (fun S ↦ S.carrier)
      { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝,
        zero_mem' := zero_mem'✝, algebraMap_mem' := algebraMap_mem'✝, star_mem' := star_mem'✝,
        centralizer_centralizer' := centralizer_centralizer'✝ } =
    (fun S ↦ S.carrier) T
⊢ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝,
      algebraMap_mem' := algebraMap_mem'✝, star_mem' := star_mem'✝,
      centralizer_centralizer' := centralizer_centralizer'✝ } =
    T