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

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
⊢ (1 - z * I)⁻¹.arg ∈ Set.Ioo (-(π / 2)) (π / 2)

Tactic:
arg_inv,

Goal state after:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
⊢ (if (1 - z * I).arg = π then π else -(1 - z * I).arg) ∈ Set.Ioo (-(π / 2)) (π / 2)
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case neg
p : ℝ
hp : p = 0 ∨ p = 1
⊢ 0 = log (1 - p) - log p

Tactic:
obtain rfl | rfl := hp <;> simp

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

Goal state before:
pp: A : Type u_1
inst✝⁸ : PartialOrder A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : SeparatelyContinuousMul A
c : A
⊢ Monotone ⇑(conjSqrt c)

Tactic:
intro a b hab

Goal state after:
A : Type u_1
inst✝⁸ : PartialOrder A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : SeparatelyContinuousMul A
c a b : A
hab : a ≤ b
⊢ (conjSqrt c) a ≤ (conjSqrt c) b
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
p : ℝ
hp : 0 < p ∧ p < 1
⊢ -1 / (p * (1 - p)) < 0

Tactic:
apply div_neg_of_neg_of_pos

Goal state after:
case ha
q : ℕ
p : ℝ
hp : 0 < p ∧ p < 1
⊢ -1 < 0

case hb
q : ℕ
p : ℝ
hp : 0 < p ∧ p < 1
⊢ 0 < p * (1 - p)
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 ∈ Icc 0 1
⊢ Monotone fun a ↦ a ^ p

Tactic:
intro a b hab

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hp : p ∈ Icc 0 1
a b : A
hab : a ≤ b
⊢ (fun a ↦ a ^ p) a ≤ (fun a ↦ a ^ p) b
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ Monotone sqrt

Tactic:
intro a b hab

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a ≤ b
⊢ sqrt a ≤ sqrt b
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: a : ℝ
⊢ Tendsto (fun n ↦ a ^ (2 * n + 1) / ↑n !) atTop (nhds 0)

Tactic:
rw [← mul_zero a]

Goal state after:
a : ℝ
⊢ Tendsto (fun n ↦ a ^ (2 * n + 1) / ↑n !) atTop (nhds (a * 0))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: case inl
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : q = 0
⊢ Monotone fun a ↦ a ^ ↑0

Tactic:
intro a b hab

Goal state after:
case inl
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : q = 0
a b : A
hab : a ≤ b
⊢ (fun a ↦ a ^ ↑0) a ≤ (fun a ↦ a ^ ↑0) b
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)
⊢ Tendsto (fun p ↦ ∫ (x : ℝ) in p.1..p.2, x⁻¹ • (f (a * x) - f (b * x))) (𝓝[>] 0 ×ˢ atTop) (𝓝 (log (b / a) • (L - R)))

Tactic:
let u := fun x ↦ x⁻¹ • f x

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
⊢ Tendsto (fun p ↦ ∫ (x : ℝ) in p.1..p.2, x⁻¹ • (f (a * x) - f (b * x))) (𝓝[>] 0 ×ˢ atTop) (𝓝 (log (b / a) • (L - R)))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: h : Tendsto (fun z ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ Tendsto (fun s ↦ 2 * ↑π ^ (-s / 2)) (𝓝[≠] 0) (𝓝 (2 * ↑π ^ (-0 / 2)))

Tactic:
refine Tendsto.mono_left (ContinuousAt.tendsto ?_) nhdsWithin_le_nhds

Goal state after:
h : Tendsto (fun z ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ ContinuousAt (fun s ↦ 2 * ↑π ^ (-s / 2)) 0
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: ⊢ 1 / 2 < eulerMascheroniSeq 6

Tactic:
have : eulerMascheroniSeq 6 = 49 / 20 - log 7 := by
    rw [eulerMascheroniSeq]
    norm_num

Goal state after:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 1 / 2 < eulerMascheroniSeq 6
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: ⊢ Tendsto eulerMascheroniSeq atTop (𝓝 eulerMascheroniConstant)

Tactic:
have := tendsto_atTop_ciSup strictMono_eulerMascheroniSeq.monotone ?_
  · rwa [eulerMascheroniConstant, this.limUnder_eq]
  · exact ⟨_, fun _ ⟨_, hn⟩ ↦ hn ▸ (eulerMascheroniSeq_lt_eulerMascheroniSeq' _ 1).le⟩

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

Goal state before:
pp: case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹

Tactic:
rw [(by ring : 2 - s = 1 - (s - 1)), inv_Gammaℝ_one_sub h',
    (by rw [sub_add_cancel] : Gammaℂ s = Gammaℂ (s - 1 + 1)), Gammaℂ_add_one h,
    (by ring : s + 1 = (s - 1) + 2), Gammaℝ_add_two h, mul_sub, sub_div, mul_one,
      Complex.cos_sub_pi_div_two]

Goal state after:
case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ (s - 1).Gammaℂ * sin (↑π * s / 2) * (s - 1).Gammaℝ⁻¹ =
    (s - 1).Gammaℂ * (s - 1) / 2 / ↑π * sin (↑π * s / 2) * ((s - 1).Gammaℝ * (s - 1) / 2 / ↑π)⁻¹
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 n : ℕ
⊢ log b ↑n = ↑(Nat.log b n)

Tactic:
cases n
  · simp [log_of_right_le_one]
  · rw [log_of_one_le_right, Nat.floor_natCast]
    simp

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

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

Tactic:
simp only [← log_div_log, log_one, div_zero]

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

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

Tactic:
by
  rw [← logb_one]
  exact logb_lt_logb_iff hb h zero_lt_one

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

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

Tactic:
log_div y_pos.ne' x_pos.ne'

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

Goal state before:
pp: case h
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 : ℕ
hn : N ≤ n
⊢ ∀ᵐ (ω : E) ∂P, ‖(u n).mulExpNegMulSq (g ω)‖ ≤ ‖g‖

Tactic:
exact Eventually.of_forall
      (fun _ => abs_mulExpNegMulSq_comp_le_norm g (le_of_lt (Set.mem_Ioi.mp (hupos n hn))))

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

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

Tactic:
setLIntegral_subtype measurableSet_Ioi _ fun a : ℝ ↦ .ofReal (a ^ n),

Goal state after:
n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
⊢ ∫⁻ (x : ℝ) in Subtype.val '' Iio x, ENNReal.ofReal (x ^ n) ∂volume = ENNReal.ofReal (↑x ^ (n + 1) / (↑n + 1))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case h₂
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ ‖2 * l‖ + ‖s‖ ≤ 2.5 * ‖l‖

Tactic:
simp only [Complex.norm_mul, Complex.norm_ofNat]

Goal state after:
case h₂
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ 2 * ‖l‖ + ‖s‖ ≤ 2.5 * ‖l‖
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: case refine_2
a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
⊢ ↑(n + 1)! = ↑n ! * (↑n + 1)

pp: case refine_3
a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
⊢ Multiset.map (fun x ↦ Gamma (x + ↑(n + 1))) b = Multiset.map (fun j ↦ Gamma (j + ↑n) * (j + ↑n)) b

Tactic:
· rw [Nat.factorial_succ]
      grind

Goal state after:
case refine_3
a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
⊢ Multiset.map (fun x ↦ Gamma (x + ↑(n + 1))) b = Multiset.map (fun j ↦ Gamma (j + ↑n) * (j + ↑n)) b
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case e'_6
m : ℕ
f : ℕ → ℝ := fun k ↦ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
⊢ log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)) + ∑ i ∈ range 1, f i = (↑(m + 1) + 1 / 2) * log (1 + (↑m + 1)⁻¹)

Tactic:
have h (x) (hx : x ≠ (0 : ℝ)) : 1 + x⁻¹ = (x + 1) / x := by field
    simp (disch := positivity) only [log_stirlingSeq_formula, log_div, log_mul, log_exp,
      factorial_succ, cast_mul, cast_succ, range_one, sum_singleton, h]
    ring

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

Goal state before:
pp: f : ℝ → ℝ
⊢ ∫ (x : ℝ), f x ∂measureT = ∫ (x : ℝ) in -1..1, f x * √(1 - x ^ 2)⁻¹

Tactic:
rw [integral_of_le (by norm_num), measureT,
    restrict_withDensity (by measurability),
    integral_withDensity_eq_integral_smul (by fun_prop)]
  congr! 2 with x hx
  simp [NNReal.smul_def, mul_comm]

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

Goal state before:
pp: n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ∫ (θ : ℝ) in 0..↑n * π, cos θ = 0

Tactic:
trans ∫ θ in 0..n * π, (deriv sin) θ

Goal state after:
n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ∫ (θ : ℝ) in 0..↑n * π, cos θ = ∫ (θ : ℝ) in 0..↑n * π, deriv sin θ

n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ∫ (θ : ℝ) in 0..↑n * π, deriv sin θ = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case inr
n i : ℕ
hi : i ∈ Finset.Iic n
hn : n ≠ 0
this : ↑↑n * (↑i * π / ↑n) = ↑i * π
⊢ cos (↑i * π) = (-1) ^ i

Tactic:
cos_nat_mul_pi

Goal state after:
case inr
n i : ℕ
hi : i ∈ Finset.Iic n
hn : n ≠ 0
this : ↑↑n * (↑i * π / ↑n) = ↑i * π
⊢ (-1) ^ i = (-1) ^ i
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℤ
x : ℝ
hx : |x| ≤ 1
h : eval x (T ℝ n) ∈ Set.Icc (-1) 1
⊢ |eval x (T ℝ n)| ≤ 1

Tactic:
exact abs_le.mpr (Set.mem_Icc.mp h)

Goal state after:
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
h✝ : ¬(1 ≤ i ∧ i ≤ n - k)
⊢ (Finset.Icc 1 (n - k)).card = n - k

Tactic:
by grind [Nat.card_Icc]

Goal state after:
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
h✝ : 1 ≤ i ∧ i ≤ n - k
⊢ ((Finset.Icc 1 (n - k + 1)).erase i).card = n - k

Tactic:
by grind [Nat.card_Icc]

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

Goal state before:
pp: case e'_3
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hk : k ≤ n
⊢ eval x ((⇑derivative)^[k] P) =
    sumNodes ?neg.convert_1✝ (fun i ↦ iterateDerivativeC ?neg.convert_1✝ (?neg.convert_2✝ i) x i) P

Tactic:
sumNodes_eq_eval_iterate_derivative hk x hPdeg

Goal state after:
case e'_3
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hk : k ≤ n
⊢ eval x ((⇑derivative)^[k] P) = eval x ((⇑derivative)^[k] P)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ meromorphicOrderAt ℘[L] l₀ = ↑(-2)

pp: L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ ↑(-2) = -2

Tactic:
· rw [meromorphicOrderAt_eq_int_iff (L.meromorphic_weierstrassP l₀)]
    refine ⟨fun z ↦ (z - l₀) ^ 2 * ℘[L - l₀] z + 1 - (z - l₀) ^ 2 / l₀ ^ 2, ?_, ?_, ?_⟩
    · have : AnalyticAt ℂ ℘[L - l₀] l₀ := L.analyticOnNhd_weierstrassPExcept l₀ l₀ (by simp)
      suffices AnalyticAt ℂ (fun z ↦ (z - l₀) ^ 2 / l₀ ^ 2) l₀ by fun_prop
      by_cases hl₀ : l₀ = 0
      · simpa [hl₀] using analyticAt_const
      · fun_prop (disch := simpa)
    · simp
    · filter_upwards [self_mem_nhdsWithin] with z (hz : _ ≠ _)
      have : (z - l₀) ^ 2 ≠ 0 := by simpa [sub_eq_zero]
      simp [← L.ite_eq_one_sub_sq_mul_weierstrassP l₀ h,
        if_neg hz, inv_mul_cancel_left₀ this, zpow_ofNat]

Goal state after:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ ↑(-2) = -2
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ iteratedDeriv 6
      (fun z ↦
        (℘'[L - 0] z * z ^ 3 - 2) ^ 2 - 4 * (℘[L - 0] z * z ^ 2 + 1) ^ 3 + L.g₂ * (℘[L - 0] z * z ^ 6 + z ^ 4) +
          L.g₃ * z ^ 6)
      0 =
    0

Tactic:
pow_succ (_ + _),

Goal state after:
L : PeriodPair
⊢ iteratedDeriv 6
      (fun z ↦
        (℘'[L - 0] z * z ^ 3 - 2) ^ 2 -
              4 *
                ((℘[L - 0] z * z ^ 2 + 1) ^ 0 * (℘[L - 0] z * z ^ 2 + 1) * (℘[L - 0] z * z ^ 2 + 1) *
                  (℘[L - 0] z * z ^ 2 + 1)) +
            L.g₂ * (℘[L - 0] z * z ^ 6 + z ^ 4) +
          L.g₃ * z ^ 6)
      0 =
    0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ ∑ x ∈ Finset.range (6 + 1),
            ↑(Nat.choose 6 x) *
                (∑ x_1 ∈ Finset.range (x + 1),
                    ↑(x.choose x_1) * (↑(x_1 + 2)! * L.sumInvPow 0 (x_1 + 3)) * ↑(if x - x_1 = 3 then 3! else 0) -
                  if x = 0 then 2 else 0) *
              (∑ x_1 ∈ Finset.range (6 - x + 1),
                  ↑((6 - x).choose x_1) * (↑(x_1 + 2)! * L.sumInvPow 0 (x_1 + 3)) *
                    ↑(if 6 - x - x_1 = 3 then 3! else 0) -
                if 6 - x = 0 then 2 else 0) -
          ∑ x ∈ Finset.range (6 + 1),
            (↑(Nat.choose 6 x) * if x = 0 then 4 else 0) *
              ∑ x_1 ∈ Finset.range (6 - x + 1),
                (↑((6 - x).choose x_1) *
                    ∑ x ∈ Finset.range (x_1 + 1),
                      ↑(x_1.choose x) *
                          (∑ x_2 ∈ Finset.range (x + 1),
                              (↑(x.choose x_2) *
                                  if x_2 = 0 then ℘[L - 0] 0 else ↑(x_2 + 1)! * L.sumInvPow 0 (x_2 + 2)) *
                                ↑(if x - x_2 = 2 then 2! else 0) +
                            if x = 0 then 1 else 0) *
                        (∑ x_2 ∈ Finset.range (x_1 - x + 1),
                            (↑((x_1 - x).choose x_2) *
                                if x_2 = 0 then ℘[L - 0] 0 else ↑(x_2 + 1)! * L.sumInvPow 0 (x_2 + 2)) *
                              ↑(if x_1 - x - x_2 = 2 then 2! else 0) +
                          if x_1 - x = 0 then 1 else 0)) *
                  (∑ x_2 ∈ Finset.range (6 - x - x_1 + 1),
                      (↑((6 - x - x_1).choose x_2) *
                          if x_2 = 0 then ℘[L - 0] 0 else ↑(x_2 + 1)! * L.sumInvPow 0 (x_2 + 2)) *
                        ↑(if 6 - x - x_1 - x_2 = 2 then 2! else 0) +
                    if 6 - x - x_1 = 0 then 1 else 0) +
        ∑ x ∈ Finset.range (6 + 1),
          (↑(Nat.choose 6 x) * if x = 0 then L.g₂ else 0) *
            (∑ x_1 ∈ Finset.range (6 - x + 1),
                (↑((6 - x).choose x_1) * if x_1 = 0 then ℘[L - 0] 0 else ↑(x_1 + 1)! * L.sumInvPow 0 (x_1 + 2)) *
                  ↑(if 6 - x - x_1 = 6 then 6! else 0) +
              ↑(if 6 - x = 4 then 4! else 0)) +
      ∑ x ∈ Finset.range (6 + 1), (↑(Nat.choose 6 x) * if x = 0 then L.g₃ else 0) * ↑(if 6 - x = 6 then 6! else 0) =
    0

Tactic:
simp [Finset.sum_range_succ, L.G_eq_zero_of_odd 3 (by decide), g₃,
    show Nat.choose 6 4 = 15 by rfl, show Nat.choose 6 3 = 20 by rfl]

Goal state after:
L : PeriodPair
⊢ -(2 * (20 * (↑5! * L.G 6) * ↑3!)) + -(20 * (↑5! * L.G 6) * ↑3! * 2) -
        4 * (15 * (↑5! * L.G 6) * 2 + (15 * (↑5! * L.G 6) * 2 + 15 * (↑5! * L.G 6) * 2)) +
      140 * L.G 6 * ↑6! =
    0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : ¬i = 0
hi₄ : ¬i = 6
⊢ iteratedDeriv i
      (fun z ↦
        (℘'[L - 0] z * z ^ 3 - 2) ^ 2 - 4 * (℘[L - 0] z * z ^ 2 + 1) ^ 3 + L.g₂ * (℘[L - 0] z * z ^ 6 + z ^ 4) +
          L.g₃ * z ^ 6)
      0 =
    0

Tactic:
pow_succ (_ + _),

Goal state after:
case neg
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : ¬i = 0
hi₄ : ¬i = 6
⊢ iteratedDeriv i
      (fun z ↦
        (℘'[L - 0] z * z ^ 3 - 2) ^ 2 -
              4 *
                ((℘[L - 0] z * z ^ 2 + 1) ^ 0 * (℘[L - 0] z * z ^ 2 + 1) * (℘[L - 0] z * z ^ 2 + 1) *
                  (℘[L - 0] z * z ^ 2 + 1)) +
            L.g₂ * (℘[L - 0] z * z ^ 6 + z ^ 4) +
          L.g₃ * z ^ 6)
      0 =
    0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
x : ℂ
l : ↥L.lattice
⊢ L.relation (x + ↑l) = L.relation x

Tactic:
simp only [relation, derivWeierstrassP_add_coe, weierstrassP_add_coe]

Goal state after:
L : PeriodPair
x : ℂ
l : ↥L.lattice
⊢ (if x + ↑l ∈ L.lattice then 0 else ℘'[L] x ^ 2 - 4 * ℘[L] x ^ 3 + L.g₂ * ℘[L] x + L.g₃) =
    if x ∈ L.lattice then 0 else ℘'[L] x ^ 2 - 4 * ℘[L] x ^ 3 + L.g₂ * ℘[L] x + L.g₃
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
⊢ arithGeom a b 0 n = b * (a ^ n - 1) / (a - 1)

Tactic:
rw [arithGeom_zero_eq_mul_div' ha n, ← neg_sub _ a, div_neg, ← neg_sub _ (a ^ n), mul_neg,
    neg_div, neg_neg]

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

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

Tactic:
have : -(n : ℤ) + 1 = -((n - 1 : ℕ) : ℤ) := by grind

Goal state after:
n : ℕ
hn0 : ¬n = 0
this : -↑n + 1 = -↑(n - 1)
⊢ (-1) ^ (n + 1) * (↑(Nat.fib n) - ↑(Nat.fib (n + 1))) = fib (-↑n + 1)
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: m n : ℤ
⊢ (fib m).gcd (fib n) = Nat.fib (m.gcd n)

Tactic:
obtain ⟨m, (rfl | rfl)⟩ := m.eq_nat_or_neg
    <;> obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
    <;> simp [fib_neg, Nat.fib_gcd, apply_ite, apply_ite_left]

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

Goal state before:
pp: case refine_1
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
⊢ (k + 2) % 2 = 1

Tactic:
rw [add_mod, mod_self, add_zero, mod_mod]
    exact h.2.1

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

Goal state before:
pp: n l : ℕ
⊢ DifferentiableOn ℂ (iteratedDerivWithin l (fun z ↦ cotTerm z n) ℍₒ) ℍₒ

Tactic:
by
  suffices DifferentiableOn ℂ (fun z : ℂ ↦ (-1) ^ l * l ! * ((z + (n + 1)) ^ (-1 - l : ℤ) +
    (z - (n + 1)) ^ (-1 - l : ℤ))) ℍₒ by
    exact this.congr fun z hz ↦ eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet l n hz
  apply DifferentiableOn.const_mul
  apply DifferentiableOn.add <;> refine DifferentiableOn.zpow (by fun_prop) <| .inl fun x hx ↦ ?_
  · simpa [add_eq_zero_iff_neg_eq'] using (UpperHalfPlane.ne_intCast (.mk x hx) (-(n + 1))).symm
  · simpa [sub_eq_zero] using (UpperHalfPlane.ne_intCast (.mk x hx) (n + 1))

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
i : ℕ
hi : ↑a ≤ ↑i ∧ ↑i + 1 ≤ ↑b
⊢ IntegrableOn g (Ico ↑i ↑(i + 1)) volume

Tactic:
exact hg.mono (by grind) le_rfl

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
i : ℕ
hi : ↑i + 1 ≤ ↑a
this : IntervalIntegrable f volume (x₀ + ↑i) (x₀ + (↑i + 1))
x✝¹ : ℝ
x✝ : x✝¹ ∈ Icc (x₀ + ↑i) (x₀ + (↑i + 1))
⊢ f x✝¹ ≤ f (x₀ + ↑i)

Tactic:
by apply hf <;> grind

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
i : ℕ
hi : ↑i + 1 ≤ ↑a
this : IntervalIntegrable f volume (x₀ + ↑i) (x₀ + (↑i + 1))
x✝¹ : ℝ
x✝ : x✝¹ ∈ Icc (x₀ + ↑i) (x₀ + (↑i + 1))
⊢ f (x₀ + (↑i + 1)) ≤ f x✝¹

Tactic:
by apply hf <;> grind

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Abelian

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject (op G)) C
T : C := Injective.under (∏ᶜ fun P ↦ unop (Subobject.underlying.obj P))
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject (op G) := Subobject.mk (factorThruImage (h ≫ f)).op
q₁ : image (h ≫ f) ⟶ unop (Subobject.underlying.obj R) :=
  (Subobject.underlyingIso (factorThruImage (h ≫ f)).op).unop.hom
q₂ : unop (Subobject.underlying.obj R) ⟶ ∏ᶜ fun P ↦ unop (Subobject.underlying.obj P) :=
  section_ (Pi.π (fun P ↦ unop (Subobject.underlying.obj P)) R)
q : image (h ≫ f) ⟶ T := q₁ ≫ q₂ ≫ Injective.ι (∏ᶜ fun P ↦ unop (Subobject.underlying.obj P))
⊢ factorThruImage (h ≫ f) ≫ q = 0

Tactic:
by rw [← Injective.comp_factorThru q (Limits.image.ι (h ≫ f)), Limits.image.fac_assoc,
      Category.assoc, hf, comp_zero]

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

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

Tactic:
have L : Tendsto (fun ε => l + ε * (1 + ε + l)) (𝓝[>] 0) (𝓝 (l + 0 * (1 + 0 + l))) := by
        apply Tendsto.mono_left _ nhdsWithin_le_nhds
        exact
          tendsto_const_nhds.add
            (tendsto_id.mul ((tendsto_const_nhds.add tendsto_id).add tendsto_const_nhds))

Goal state after:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
d : ℝ
hd : d > l
L : Tendsto (fun ε ↦ l + ε * (1 + ε + l)) (𝓝[>] 0) (𝓝 (l + 0 * (1 + 0 + l)))
⊢ ∃ ε, l + ε * (1 + ε + l) < d ∧ 0 < ε
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
⊢ c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹

Tactic:
rw [← div_eq_mul_inv, ← div_eq_mul_inv, div_le_div_iff₀ _ (sub_pos.2 hc)]

Goal state after:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
⊢ c ^ 2 * (c - 1) ≤ c ^ 3 * (1 - c⁻¹ ^ 2)

N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
⊢ 0 < 1 - c⁻¹ ^ 2