mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 0 1
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₀₁ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₀₁ t x ∂μ
a : A
ha : 0 ≤ a
a✝ : Nontrivial A
p_pos : 0 < ↑p
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₀₁ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p).rpowIntegrand₀₁ x 0 = 0
⊢ a ^ p = cfcₙ (fun r ↦ ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₀₁ t r ∂μ) a

Tactic:
by
      rw [nnrpow_eq_cfcₙ_real _ _]
      exact cfcₙ_congr fun r _ ↦ (hμ r (by grind)).2

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℝ
ha : 0 < a
s : ℝ
⊢ Tendsto (fun x ↦ |x| ^ s * rexp (-a * x ^ 2)) (cocompact ℝ) (𝓝 0)

Tactic:
conv in rexp _ => rw [← sq_abs]
  rw [cocompact_eq_atBot_atTop, ← comap_abs_atTop]
  erw [tendsto_comap'_iff (m := fun y => y ^ s * rexp (-a * y ^ 2))
      (mem_atTop_sets.mpr ⟨0, fun b hb => ⟨b, abs_of_nonneg hb⟩⟩)]
  exact
    (rpow_mul_exp_neg_mul_sq_isLittleO_exp_neg ha s).tendsto_zero_of_tendsto
      (tendsto_exp_atBot.comp <| tendsto_id.const_mul_atTop_of_neg (neg_lt_zero.mpr one_half_pos))

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

Goal state before:
pp: h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ √π * (-2 * γ + deriv (fun s ↦ 2 ^ (1 - 2 * s)) (1 / 2) + γ) = √π * (-2 * γ + -(2 * log 2) + γ)

Tactic:
congr 3
    apply HasDerivAt.deriv
    have := HasDerivAt.rpow (hasDerivAt_const (1 / 2 : ℝ) (2 : ℝ))
      (?_ : HasDerivAt (fun s : ℝ ↦ 1 - 2 * s) (-2) (1 / 2)) two_pos
    · simpa
    simp_rw [mul_comm (2 : ℝ) _]
    apply HasDerivAt.const_sub
    exact hasDerivAt_mul_const (2 : ℝ)

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

Goal state before:
pp: case inr.inr
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 : r < 1
⊢ r < ↑b ^ (-↑(Nat.clog b ⌈r⁻¹⌉₊) + 1)

Tactic:
have hcri : 1 < r⁻¹ := (one_lt_inv₀ hr).2 hr1

Goal state after:
case inr.inr
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 : r < 1
hcri : 1 < r⁻¹
⊢ r < ↑b ^ (-↑(Nat.clog b ⌈r⁻¹⌉₊) + 1)
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (↑b ^ ↑n) = ↑n

pp: case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (↑b ^ (-↑n)) = -↑n

Tactic:
· rw [log_of_one_le_right _ (one_le_zpow₀ (mod_cast hb.le) <| Int.natCast_nonneg _), zpow_natCast,
      ← Nat.cast_pow, Nat.floor_natCast, Nat.log_pow hb]

Goal state after:
case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (↑b ^ (-↑n)) = -↑n
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 : ℕ
hb : 1 < b
z : ℤ
⊢ log b (↑b ^ z) = z

Tactic:
by
  obtain ⟨n, rfl | rfl⟩ := Int.eq_nat_or_neg z
  · rw [log_of_one_le_right _ (one_le_zpow₀ (mod_cast hb.le) <| Int.natCast_nonneg _), zpow_natCast,
      ← Nat.cast_pow, Nat.floor_natCast, Nat.log_pow hb]
  · rw [log_of_right_le_one _ (zpow_le_one_of_nonpos₀ (mod_cast hb.le) <|
      neg_nonpos.2 (Int.natCast_nonneg _)),
      zpow_neg, inv_inv, zpow_natCast, ← Nat.cast_pow, Nat.ceil_natCast, Nat.clog_pow _ _ hb]

Goal state after:
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
⊢ b ∈ Ici 0 → a ≤ b → cfcₙ (p.rpowIntegrand₀₁ t) a ≤ cfcₙ (p.rpowIntegrand₀₁ t) b

Tactic:
(hb : 0 ≤ b)

Goal state after:
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
⊢ a ≤ b → cfcₙ (p.rpowIntegrand₀₁ t) a ≤ cfcₙ (p.rpowIntegrand₀₁ t) b
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

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

pp: b x : ℝ
hb : 1 < b
h : 0 < x
⊢ ℝ

Tactic:
exact logb_lt_logb_iff hb h zero_lt_one

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
hynonneg : 0 ≤ y
⊢ 1 ≤ rexp y + 2 * y

Tactic:
exact le_trans (one_le_exp hynonneg) (le_add_of_nonneg_right (by simp [hynonneg]))

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

Goal state before:
pp: ⊢ AntitoneOn (fun x ↦ log x / √x) (Ici (rexp 2))

Tactic:
simp_rw [sqrt_eq_rpow]

Goal state after:
⊢ AntitoneOn (fun x ↦ log x / x ^ (1 / 2)) (Ici (rexp 2))
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x y : ℝ
⊢ dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y

Tactic:
have h := lipschitzWith_one_mulExpNegMulSq hε x y
  rwa [ENNReal.coe_one, one_mul, ← (toReal_le_toReal (edist_ne_top _ _) (edist_ne_top _ _))] at h

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

Goal state before:
pp: b x : ℝ
hb₀ : 0 < b
hb : b ≠ 1
⊢ ContinuousAt (logb b) x ↔ x ≠ 0

Tactic:
by
  refine ⟨?_, continuousAt_logb⟩
  rintro h rfl
  cases lt_or_gt_of_ne hb with
  | inl hb₁ =>
      exact not_tendsto_nhds_of_tendsto_atTop (tendsto_logb_nhdsNE_zero_of_base_lt_one hb₀ hb₁)
        _ (h.tendsto.mono_left inf_le_left)
  | inr hb₁ =>
      exact not_tendsto_nhds_of_tendsto_atBot (tendsto_logb_nhdsNE_zero hb₁)
        _ (h.tendsto.mono_left inf_le_left)

Goal state after:
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
f : X →ᵇ E
⊢ ∫⁻ (x : X), ↑‖f‖₊ ∂μ = ↑‖f‖₊ * μ Set.univ

Tactic:
rw [lintegral_const]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
⊢ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed ↔ μ.InnerRegularWRT IsCompact IsClosed

Tactic:
constructor <;> intro h A hA r hr

Goal state after:
case mp
α : 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 ⊆ A, IsCompact K ∧ r < μ K

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 ⊆ A, (IsCompact ∘ closure) K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
⊢ μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed ↔ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed

Tactic:
constructor <;> intro h A hA r hr

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

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 ⊆ A, (fun s ↦ IsCompact s ∧ IsClosed s) K ∧ r < μ K
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
⊢ μ.toSphere univ < ∞

Tactic:
rw [toSphere_apply_univ']

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
⊢ ↑(dim E) * μ (ball 0 1 \ {0}) < ∞
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
⊢ DifferentiableOn ℂ ℘[L - l₀] (↑L.lattice \ {l₀})ᶜ

Tactic:
refine (L.hasSumLocallyUniformly_weierstrassPExcept l₀).hasSumLocallyUniformlyOn.differentiableOn
    (.of_forall fun s ↦ .fun_sum fun i hi ↦ ?_) L.isOpen_compl_lattice_sdiff
  split_ifs
  · simp
  · exact .sub (.div (by fun_prop) (by fun_prop) (by aesop (add simp sub_eq_zero))) (by fun_prop)

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

Goal state before:
pp: case h
a b : Multiset ℂ
h : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
n : ℕ
hn : (b.toFinset.sup fun x ↦ ⌈-x.re⌉₊) + 1 ≤ n
h' : regularizedHGFunCoeff a b n = 0
⊢ False

Tactic:
rw [regularizedHGFunCoeff_eq_zero_iff] at h'

Goal state after:
case h
a b : Multiset ℂ
h : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
n : ℕ
hn : (b.toFinset.sup fun x ↦ ⌈-x.re⌉₊) + 1 ≤ n
h' : (∃ j ∈ a, ∃ k < n, j = -↑k) ∨ ∃ j ∈ b, ∃ m, j + ↑n = -↑m
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
x : ℂ
hx : x ∈ L.lattice → x + ↑l = l₀
H : x + ↑l ∈ L.lattice
⊢ x ∈ L.lattice

Tactic:
by simpa using sub_mem H l.2

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

Goal state before:
pp: case a
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
x : ℂ
hx : x ∈ L.lattice → x + ↑l = l₀
⊢ x + ↑l ∈ L.lattice → x + ↑l = l₀

Tactic:
exact fun H ↦ hx (by simpa using sub_mem H l.2)

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

Goal state before:
pp: ⊢ stirlingSeq 0 = 0

Tactic:
rw [stirlingSeq, cast_zero, mul_zero, Real.sqrt_zero, zero_mul, div_zero]

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

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
⊢ NNReal.mk √(1 - x ^ 2)⁻¹ ⋯ • f x = f x * √(1 - x ^ 2)⁻¹

Tactic:
simp [NNReal.smul_def, mul_comm]

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

Goal state before:
pp: f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this : IntervalIntegrable (fun x ↦ f x * √(1 - x ^ 2)⁻¹) volume (-1) 1
⊢ Integrable f measureT

Tactic:
intervalIntegrable_iff,

Goal state after:
f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this : IntegrableOn (fun x ↦ f x * √(1 - x ^ 2)⁻¹) (Set.uIoc (-1) 1) volume
⊢ Integrable f measureT
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
⊢ Int.fract r ∈ {0, 1 / 3, 1 / 2, 2 / 3}

Tactic:
suffices Int.fract r ∈ ({0, 1 / 3, 1 / 2, 2 / 3, 1} : Set ℚ) by
    grind [ne_of_lt (Int.fract_lt_one r)]
  refine niven_angle_div_pi_eq (r := Int.fract r) ?_ (by simp [le_of_lt <| Int.fract_lt_one r])
  obtain ⟨q, hq⟩ := hcos
  exact ⟨(-1) ^ ⌊r⌋ * q, by rw [Int.fract]; push_cast; rw [sub_mul, cos_sub_int_mul_pi, hq]⟩

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

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

Tactic:
H0,

Goal state after:
x : Fin 2 → ℤ
hx : ↑(x 0).natAbs ≠ 0
H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs
⊢ x 0 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
hn : n ≠ 0
k : ℕ
hk : k ≤ n
⊢ ↑↑k * π = ↑↑n * (↑k * π / ↑n)

Tactic:
by simp [field]

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

Goal state before:
pp: n : ℕ
x : ℝ
hroot : (T ℝ ↑n).IsRoot x
hnz : x ≠ 0
⊢ Irrational x

Tactic:
rw [← mem_roots (T_ne_zero ℝ n), roots_T_real, Finset.mem_val] at hroot
  obtain ⟨k, hk₁, hk₂⟩ := Finset.mem_image.mp hroot
  have hn : n ≠ 0 := by grind
  suffices Irrational (cos ((Rat.divInt (2 * k + 1) (2 * n)) * π)) by
    rw [← hk₂]; convert! this using 2; push_cast; field_simp
  apply irrational_cos_rat_mul_pi
  contrapose! hnz
  have : (Rat.divInt (2 * k + 1) (2 * n)).den = 2 * (n / n.gcd (2 * k + 1)) := calc
    _ = 2 * n / (2 * n).gcd (2 * k + 1) := by rw [Rat.den_divInt]; norm_cast; simp [hn]
    _ = _ := by rw [Nat.Coprime.gcd_mul_left_cancel n (by simp),
      Nat.mul_div_assoc _ (Nat.gcd_dvd_left ..)]
  have hn : 2 * k + 1 = n := Nat.eq_of_dvd_of_lt_two_mul (by simp) (Nat.gcd_eq_left_iff_dvd.mp <|
    Nat.eq_of_dvd_of_div_eq_one (Nat.gcd_dvd_left ..) (by grind [Rat.den_pos])) (by grind)
  rw_mod_cast [← hk₂, hn]; convert! cos_pi_div_two using 2; push_cast; field_simp

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

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

Tactic:
rw [fib_natCast_add]; grind

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) + n) =
    fib (↑m - 1) * fib n + fib ↑m * fib (n + 1) + fib ↑m * fib n + fib (↑m + 1) * fib (n + 1)

Tactic:
rw [fib_natCast_add]; grind

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

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

Tactic:
rw [fib_natCast_add]; grind

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 + 1) + n) =
    fib (↑m - 1) * fib n + fib ↑m * fib (n + 1) + fib ↑m * fib n + fib (↑m + 1) * fib (n + 1)

Tactic:
rw [fib_natCast_add]; grind

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

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
this : Summable fun i ↦ (x - ↑i)⁻¹ * (x + ↑i)⁻¹
⊢ Summable fun i ↦ 1 / ((x + (↑i + 1)) * (x - (↑i + 1)))

Tactic:
← summable_nat_add_iff 1

Goal state after:
x : ℂ
hz : x ∈ ℂ_ℤ
this : Summable fun n ↦ (x - ↑(n + 1))⁻¹ * (x + ↑(n + 1))⁻¹
⊢ Summable fun i ↦ 1 / ((x + (↑i + 1)) * (x - (↑i + 1)))
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: case inl
k : ℕ
h : MinFacHelper 0 k
this : 2 < minFac 0
⊢ 1 < 0

Tactic:
contradiction

Goal state after:
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n ↦ u n / ↑n)
n : ℕ
hn : n ≠ 0
⊢ h.lim ≤ u n / ↑n

Tactic:
by
  rw [Subadditive.lim]
  exact csInf_le (hbdd.mono <| image_subset_range _ _) ⟨n, hn.bot_lt, rfl⟩

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

Goal state before:
pp: z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot - 1 / x) ℍₒ z =
    -(-1) ^ k * ↑k ! * z ^ (-1 - ↑k) + (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k)

Tactic:
simp only [← aux_iteratedDeriv_tsum_cotTerm hk hz, one_div, neg_mul, neg_add_cancel_left]

Goal state after:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot - x⁻¹) ℍₒ z =
    iteratedDerivWithin k (fun z ↦ ∑' (n : ℕ), cotTerm z n) ℍₒ z
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k M : ℕ
c : ℝ
hc : 0 < c
A : ∀ (i : ℕ), 2 ^ (-(c * ↑i)) = rexp (-(log 2 * c) * ↑i)
⊢ ∑ i ≤ M, ↑i ^ k * 2 ^ (-(c * ↑i)) ≤ 2 ^ c * ↑k ! / (log 2 * c) ^ (k + 1)

Tactic:
simp only [A, neg_mul]

Goal state after:
k M : ℕ
c : ℝ
hc : 0 < c
A : ∀ (i : ℕ), 2 ^ (-(c * ↑i)) = rexp (-(log 2 * c) * ↑i)
⊢ ∑ x ≤ M, ↑x ^ k * rexp (-(log 2 * c * ↑x)) ≤ 2 ^ c * ↑k ! / (log 2 * c) ^ (k + 1)
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
integrable : IntegrableOn f (Ioi ↑N) volume
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
M : ℕ
⊢ ∑ i ∈ Finset.range M, f ↑(i + (N + 1)) = ∑ n ∈ Finset.Ico N (N + M), f ↑(n + 1)

Tactic:
rw [Finset.sum_Ico_eq_sum_range]

Goal state after:
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
integrable : IntegrableOn f (Ioi ↑N) volume
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
M : ℕ
⊢ ∑ i ∈ Finset.range M, f ↑(i + (N + 1)) = ∑ k ∈ Finset.range (N + M - N), f ↑(N + k + 1)
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Set.Ici ↑N)
integrable : IntegrableOn f (Set.Ioi ↑N) volume
nonneg : ∀ t ∈ Set.Ioi ↑N, 0 ≤ f t
s : Finset ℕ
t : ℕ
ht : s ⊆ Finset.range t
⊢ ∑ i ∈ Finset.range t, f ↑(i + N + 1) = ∑ i ∈ Finset.Ico N (N + t), f ↑(i + 1)

Tactic:
rw [Finset.sum_Ico_eq_sum_range]

Goal state after:
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Set.Ici ↑N)
integrable : IntegrableOn f (Set.Ioi ↑N) volume
nonneg : ∀ t ∈ Set.Ioi ↑N, 0 ≤ f t
s : Finset ℕ
t : ℕ
ht : s ⊆ Finset.range t
⊢ ∑ i ∈ Finset.range t, f ↑(i + N + 1) = ∑ k ∈ Finset.range (N + t - N), f ↑(N + k + 1)
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
lim : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f ↑(i + N)) atTop (nhds (∑' (i : ℕ), f ↑(i + N)))
this : Tendsto (fun x ↦ ↑x + ↑N) atTop atTop
integrable : IntegrableOn f (Ioi ↑N) volume
M : ℕ
⊢ ∑ n ∈ Finset.Ico N (N + M), f ↑n = ∑ i ∈ Finset.range M, f ↑(i + N)

Tactic:
rw [Finset.sum_Ico_eq_sum_range]

Goal state after:
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
lim : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f ↑(i + N)) atTop (nhds (∑' (i : ℕ), f ↑(i + N)))
this : Tendsto (fun x ↦ ↑x + ↑N) atTop atTop
integrable : IntegrableOn f (Ioi ↑N) volume
M : ℕ
⊢ ∑ k ∈ Finset.range (N + M - N), f ↑(N + k) = ∑ i ∈ Finset.range M, f ↑(i + N)
Module: Mathlib.CategoryTheory.Limits.Indization.IndObject

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
inst✝¹ : IsFiltered (CostructuredArrow yoneda A)
inst✝ : FinallySmall (CostructuredArrow yoneda A)
⊢ IsIndObject A

Tactic:
have h₁ : (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙
      inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final := Functor.final_of_natIso
    (factoringCompInclusion (fromFinalModel <| CostructuredArrow yoneda A)).symm

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
inst✝¹ : IsFiltered (CostructuredArrow yoneda A)
inst✝ : FinallySmall (CostructuredArrow yoneda A)
h₁ :
  (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙
      inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
⊢ IsIndObject A
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape I (Type u₂)
A : C
i : I
⊢ ((coyonedaOpColimitIsoLimitCoyoneda' F).hom ≫ limit.π (F.rightOp ⋙ coyoneda) i).app A =
    (yoneda.obj A).map (colimit.ι F (op i)).op

Tactic:
coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π,

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape I (Type u₂)
A : C
i : I
⊢ (coyoneda.map (colimit.ι F (op i)).op).app A = (yoneda.obj A).map (colimit.ι F (op i)).op
Module: Mathlib.CategoryTheory.Limits.Indization.Category

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ RepresentablyCoflat Ind.yoneda

Tactic:
refine ⟨fun X => ?_⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : Ind C
⊢ IsFiltered (CostructuredArrow Ind.yoneda X)
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
α : Type u_3
I : α → Type u_4
inst✝³ : (i : α) → Category.{u_5, u_4} (I i)
inst✝² : HasLimitsOfShape (Discrete α) C
F : (i : α) → I i ⥤ D ⥤ C
inst✝¹ : ∀ (i : α), HasColimitsOfShape (I i) C
inst✝ : HasColimitsOfShape ((i : α) → I i) C
d : D
s : α
k : (i : α) → I i
⊢ colimit.ι (pointwiseProduct F ⋙ (evaluation D C).obj d) k ≫
      (((colimitObjIsoColimitCompEvaluation (pointwiseProduct F) d).inv ≫
            (colimitPointwiseProductToProductColimit F).app d) ≫
          (piObjIso (fun x ↦ colimit (F x)) d).hom) ≫
        Pi.π (fun x ↦ (colimit (F x)).obj d) s =
    colimit.ι (pointwiseProduct F ⋙ (evaluation D C).obj d) k ≫
      (((HasColimit.isoOfNatIso (pointwiseProductCompEvaluation F d)).hom ≫
            colimitPointwiseProductToProductColimit fun s ↦ F s ⋙ (evaluation D C).obj d) ≫
          (Pi.mapIso fun x ↦ (colimitObjIsoColimitCompEvaluation (F x) d).symm).hom) ≫
        Pi.π (fun x ↦ (colimit (F x)).obj d) s

Tactic:
simp [← NatTrans.comp_app, Functor.pi]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
this✝³ : (preadditiveCoyonedaObj G).PreservesInjectiveObjects
this✝² : (tensorObj G).PreservesMonomorphisms
this✝¹ : PreservesBinaryBiproducts (tensorObj G)
this✝ : (tensorObj G).Additive
this : (tensorObj G).PreservesHomology
⊢ PreservesFiniteLimits (tensorObj G)

Tactic:
exact (tensorObj G).preservesFiniteLimits_of_preservesHomology

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
⊢ { X₁ := I.cocomplex.X 0, X₂ := I.cocomplex.X (0 + 1), X₃ := I.cocomplex.X (0 + 2), f := I.cocomplex.d 0 (0 + 1),
            g := I.cocomplex.d (0 + 1) (0 + 2), zero := ⋯ }.f ≫
        f.f 1 -
      { X₁ := I.cocomplex.X 0, X₂ := I.cocomplex.X (0 + 1), X₃ := I.cocomplex.X (0 + 2), f := I.cocomplex.d 0 (0 + 1),
            g := I.cocomplex.d (0 + 1) (0 + 2), zero := ⋯ }.f ≫
        descHomotopyZeroZero f comm ≫ J.cocomplex.d 0 1 =
    0

Tactic:
comp_descHomotopyZeroZero_assoc f comm,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
⊢ { X₁ := I.cocomplex.X 0, X₂ := I.cocomplex.X (0 + 1), X₃ := I.cocomplex.X (0 + 2), f := I.cocomplex.d 0 (0 + 1),
            g := I.cocomplex.d (0 + 1) (0 + 2), zero := ⋯ }.f ≫
        f.f 1 -
      f.f 0 ≫ J.cocomplex.d 0 1 =
    0
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
I : InjectiveResolution X
J : InjectiveResolution Y
K : InjectiveResolution Z
⊢ Homotopy (desc (f ≫ g) K I) (desc f J I ≫ desc g K J)

Tactic:
apply descHomotopy (f ≫ g) <;> simp

Goal state after: