mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ IntegrableOn (fun t ↦ p.rpowIntegrand₀₁ t x) (Ioi 0) (C • volume)

pp: case refine_2
p : ℝ
hp : p ∈ Ioo 0 1
C : ℝ≥0 := NNReal.mk (∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1)⁻¹ ⋯
x : ℝ
hx : x ∈ Ici 0
⊢ x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x ∂C • volume

Tactic:
· unfold IntegrableOn
    rw [Measure.restrict_smul]
    exact Integrable.smul_measure_nnreal <| integrableOn_rpowIntegrand₀₁_Ioi hp hx

Goal state after:
case refine_2
p : ℝ
hp : p ∈ Ioo 0 1
C : ℝ≥0 := NNReal.mk (∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1)⁻¹ ⋯
x : ℝ
hx : x ∈ Ici 0
⊢ x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x ∂C • volume
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℝ
ha : 0 < a
⊢ 0 < (↑a).re

Tactic:
ofReal_re

Goal state after:
a : ℝ
ha : 0 < a
⊢ 0 < a
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 : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : 1 ≤ r₁
h₂ : 1 ≤ r₂
⊢ log b r₁ ≤ log b r₂

Tactic:
· 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: a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ (logb (a * b) c)⁻¹ = (logb a c)⁻¹ + (logb b c)⁻¹

Tactic:
simp_rw [inv_logb]

Goal state after:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ logb c (a * b) = logb c a + logb c b
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ (logb (a / b) c)⁻¹ = (logb a c)⁻¹ - (logb b c)⁻¹

Tactic:
simp_rw [inv_logb]

Goal state after:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ logb c (a / b) = logb c a - logb c b
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

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

Tactic:
exact log_lt_log hx hxy

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
⊢ log x < log y

Tactic:
exact log_lt_log hx hxy

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

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

Tactic:
logb_pos_iff_of_base_lt_one b_pos b_lt_one hx

Goal state after:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' : x < 1
⊢ x < 1
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X →ᵇ ℝ≥0
⊢ ∫⁻ (x : X), ↑(f x) ∂μ < ∞

Tactic:
apply IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X →ᵇ ℝ≥0
⊢ ∃ c, ∀ (x : X), ↑(f x) ≤ ↑c
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact (closure K) ∧ μ Kᶜ < ε
⊢ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed

Tactic:
refine innerRegularWRT_of_exists_compl_lt (fun s t hs ht ↦ ?_) hμ

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact (closure K) ∧ μ Kᶜ < ε
s t : Set α
hs : (IsCompact ∘ closure) s
ht : IsClosed t
⊢ (IsCompact ∘ closure) (s ∩ t)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: case pos
n a fuel : ℕ
ih : ∀ {guess : ℕ}, a < (guess + 1) ^ (n + 2) → a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
h : (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
⊢ a < (go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2)) + 1) ^ (n + 2)

pp: case neg
n a fuel : ℕ
ih : ∀ {guess : ℕ}, a < (guess + 1) ^ (n + 2) → a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
h : ¬(a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
⊢ a < (guess + 1) ^ (n + 2)

Tactic:
case pos =>
      rcases eq_or_ne guess 0 with rfl | hguess
      · grind
      · exact ih <| Nat.nthRoot.lt_pow_go_succ_aux hguess

Goal state after:
case neg
n a fuel : ℕ
ih : ∀ {guess : ℕ}, a < (guess + 1) ^ (n + 2) → a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
h : ¬(a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
⊢ a < (guess + 1) ^ (n + 2)
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: ⊢ regularizedHGFun 0 0 = cexp

Tactic:
rw [exp_eq_exp_ℂ, NormedSpace.exp_eq_expSeries_sum (𝕂 := ℂ)]
  unfold regularizedHGFun
  simp

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

Goal state before:
pp: ⊢ Continuous sigmoid

Tactic:
apply Differentiable.continuous (𝕜 := ℝ)  -- fun_prop can't choose `𝕜`
  fun_prop

Goal state after:
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
⊢ ℘[L] (-(↑l / 2) + ↑l) + (1 / ↑⟨l₀, hl₀⟩ ^ 2 - 1 / (-(↑l / 2) + ↑l - ↑⟨l₀, hl₀⟩) ^ 2) =
    ℘[L] (↑l / 2) + (1 / ↑⟨-(l₀ - ↑l), ⋯⟩ ^ 2 - 1 / (↑l / 2 - ↑⟨-(l₀ - ↑l), ⋯⟩) ^ 2) + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2)

Tactic:
add_assoc

Goal state after:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ ℘[L] (-(↑l / 2) + ↑l) + (1 / ↑⟨l₀, hl₀⟩ ^ 2 - 1 / (-(↑l / 2) + ↑l - ↑⟨l₀, hl₀⟩) ^ 2) =
    ℘[L] (↑l / 2) + (1 / ↑⟨-(l₀ - ↑l), ⋯⟩ ^ 2 - 1 / (↑l / 2 - ↑⟨-(l₀ - ↑l), ⋯⟩) ^ 2 + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2))
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: case inr.hint
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
⊢ IntervalIntegrable (deriv f) volume a b

Tactic:
have := (h.derivWithin (m := 0) (uniqueDiffOn_Icc h'ab) (by simp)).continuousOn
    apply (this.intervalIntegrable_of_Icc (μ := volume) hab).congr_ae
    simp only [hab, uIoc_of_le]
    rw [← restrict_Ioo_eq_restrict_Ioc]
    filter_upwards [self_mem_ae_restrict measurableSet_Ioo] with x hx
    exact derivWithin_of_mem_nhds (Icc_mem_nhds hx.1 hx.2)

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

Goal state before:
pp: case e'_5
m : ℕ
f : ℕ → ℝ := fun k ↦ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
⊢ f = fun i ↦ (↑(m + 1) + 1 / 2) * (2 * (1 / (2 * ↑i + 1)) * (1 / (2 * (↑m + 1) + 1)) ^ (2 * i + 1))

Tactic:
ext k

Goal state after:
case e'_5
m : ℕ
f : ℕ → ℝ := fun k ↦ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
k : ℕ
⊢ f k = (↑(m + 1) + 1 / 2) * (2 * (1 / (2 * ↑k + 1)) * (1 / (2 * (↑m + 1) + 1)) ^ (2 * k + 1))
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
g :
  HasSum (fun k ↦ ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))
k : ℕ
⊢ 1 / (2 * ↑(k + 1) + 1) * ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1) ≤ ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1)

Tactic:
refine mul_le_of_le_one_left (pow_nonneg h_nonneg ↑(k + 1)) ?_

Goal state after:
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
g :
  HasSum (fun k ↦ ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))
k : ℕ
⊢ 1 / (2 * ↑(k + 1) + 1) ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
r : ℝ := (1 / (2 * (↑n + 1) + 1)) ^ 2
hr : r = (1 / (2 * (↑n + 1) + 1)) ^ 2
hr1 : r < 1
this : HasSum (fun j ↦ r ^ (j + 1) / 3) (1 / (12 * ↑(n + 1) * (↑(n + 1) + 1)))
⊢ log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 1 + 1)) ≤ 1 / (12 * ↑(n + 1) * (↑(n + 1) + 1))

Tactic:
refine hasSum_le (fun j ↦ ?_) (log_stirlingSeq_sdiff_hasSum n) this

Goal state after:
n : ℕ
r : ℝ := (1 / (2 * (↑n + 1) + 1)) ^ 2
hr : r = (1 / (2 * (↑n + 1) + 1)) ^ 2
hr1 : r < 1
this : HasSum (fun j ↦ r ^ (j + 1) / 3) (1 / (12 * ↑(n + 1) * (↑(n + 1) + 1)))
j : ℕ
⊢ 1 / (2 * ↑(j + 1) + 1) * ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (j + 1) ≤ r ^ (j + 1) / 3
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

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

Tactic:
refine integral_congr <| fun x hx => (congrFun deriv_sin x).symm

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

Goal state before:
pp: n : ℤ
hn : n ≠ 0
⊢ ∫ (x : ℝ), eval x (T ℝ n) ∂measureT = 0

Tactic:
have hn' : (n : ℝ) ≠ 0 := Int.cast_ne_zero.mpr hn
  suffices ∫ θ in 0..n * π, cos θ = 0 by
    rw [integral_measureT_eq_integral_cos]
    simp_rw [T_real_cos]
    rwa [integral_comp_mul_left _ (Int.cast_ne_zero.mpr hn), smul_eq_zero_iff_right (by aesop),
      mul_zero]
  trans ∫ θ in 0..n * π, (deriv sin) θ
  · refine integral_congr <| fun x hx => (congrFun deriv_sin x).symm
  by_cases! 0 ≤ n
  case pos => rw [integral_deriv_of_contDiffOn_Icc contDiff_sin.contDiffOn (by positivity)]; simp
  case neg hn =>
    rw [integral_symm, integral_deriv_of_contDiffOn_Icc contDiff_sin.contDiffOn]
    · simp
    exact mul_nonpos_of_nonpos_of_nonneg (Int.cast_nonpos.mpr <| le_of_lt hn) pi_nonneg

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
x : α
h₁ : IsIntegral ℤ x
⊢ (∃ q, x = ↑q) ↔ ∃ k, x = ↑k

Tactic:
refine ⟨?_, fun ⟨w, h⟩ ↦ ⟨w, by simp [h]⟩⟩

Goal state after:
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
x : α
h₁ : IsIntegral ℤ x
⊢ (∃ q, x = ↑q) → ∃ k, x = ↑k
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ cexp (↑q * ↑π * I) ^ (2 * q.den) = 1

Tactic:
by
  nth_rw 1 [← q.num_div_den, ← exp_nat_mul]
  push_cast
  rw [show 2 * q.den * (q.num / q.den * π * I) = q.num * (2 * π * I) by field,
    exp_int_mul_two_pi_mul_I]

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

Goal state before:
pp: n : ℕ
P : ℝ[X]
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : ¬P = 0
d : ℕ
hd : ↑d = P.degree
hPdeg : d ≤ n
⊢ P.leadingCoeff ≤ 2 ^ (n - 1)

Tactic:
rw [leadingCoeff, natDegree_eq_of_degree_eq_some hd.symm]

Goal state after:
n : ℕ
P : ℝ[X]
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : ¬P = 0
d : ℕ
hd : ↑d = P.degree
hPdeg : d ≤ n
⊢ P.coeff d ≤ 2 ^ (n - 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
d : ℕ
hd : ↑d = P.degree
hPdeg : ↑d ≤ ↑n
hP : ↑d < ↑n
⊢ P.leadingCoeff < 2 ^ (n - 1)

Tactic:
have : d - 1 < n - 1 := by grind [Nat.cast_withBot, WithBot.coe_le_coe, WithBot.coe_lt_coe]

Goal state after:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
d : ℕ
hd : ↑d = P.degree
hPdeg : ↑d ≤ ↑n
hP : ↑d < ↑n
this : d - 1 < n - 1
⊢ P.leadingCoeff < 2 ^ (n - 1)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
⊢ HasFPowerSeriesOnBall ℘'[L - l₀] (L.derivWeierstrassPExceptSeries l₀ x) x ↑r

Tactic:
by
  refine .congr ?_
    ((L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept l₀).mono (.trans ?_ hr))
  · have := (L.hasFPowerSeriesOnBall_weierstrassPExcept l₀ x r hr0 hr).fderiv
    convert! (ContinuousLinearMap.apply ℂ ℂ (1 : ℂ)).comp_hasFPowerSeriesOnBall this
    ext n
    simp [weierstrassPExceptSeries, derivWeierstrassPExceptSeries]
    ring
  · simpa using Metric.ball_subset_closedBall

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

Goal state before:
pp: case refine_1
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)
⊢ eval x (T ℝ ↑n) = 0

Tactic:
obtain ⟨k, hk, hx⟩ := Finset.mem_image.mp hx
    rw [← hx, T_real_cos, cos_eq_zero_iff]
    use k
    field_simp
    norm_cast

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

Goal state before:
pp: case refine_2
n : ℕ
hn : n ≠ 0
⊢ ↑n = ↑(↑n).natAbs

pp: case refine_2
n : ℕ
hn : n ≠ 0
⊢ Set.InjOn (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) ↑(Finset.range n)

Tactic:
Int.natAbs_natCast

Goal state after:
case refine_2
n : ℕ
hn : n ≠ 0
⊢ ↑n = ↑n

case refine_2
n : ℕ
hn : n ≠ 0
⊢ Set.InjOn (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) ↑(Finset.range n)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case h
z : ℍ
a b : ℤ
h0 : z ∈ verticalStrip |z.re| z.im
⊢ ∀ᶠ (x : Fin 2 → ℤ) in cofinite,
    ‖((↑(x 0) + ↑a) * ↑z + ↑(x 1) + ↑b)⁻¹‖ ≤
      ‖r { coe := { re := |z.re|, im := z.im }, coe_im_pos := ⋯ }‖⁻¹ * ‖‖![x 0 + a, x 1 + b]‖⁻¹‖

Tactic:
filter_upwards with m

Goal state after:
case h
z : ℍ
a b : ℤ
h0 : z ∈ verticalStrip |z.re| z.im
m : Fin 2 → ℤ
⊢ ‖((↑(m 0) + ↑a) * ↑z + ↑(m 1) + ↑b)⁻¹‖ ≤
    ‖r { coe := { re := |z.re|, im := z.im }, coe_im_pos := ⋯ }‖⁻¹ * ‖‖![m 0 + a, m 1 + b]‖⁻¹‖
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: case succ
R : Type u_1
a b u₀ : R
inst✝ : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
⊢ a * a ^ n * u₀ + a * (b * ∑ k ∈ Finset.range n, a ^ k) + b = a * a ^ n * u₀ + b * ∑ k ∈ Finset.range (1 + n), a ^ k

Tactic:
add_assoc

Goal state after:
case succ
R : Type u_1
a b u₀ : R
inst✝ : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
⊢ a * a ^ n * u₀ + (a * (b * ∑ k ∈ Finset.range n, a ^ k) + b) = a * a ^ n * u₀ + b * ∑ k ∈ Finset.range (1 + n), a ^ k
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 b n = b * (1 - a ^ (n + 1)) / (1 - a)

Tactic:
by
  rw [arithGeom_eq ha n]
  field [sub_ne_zero.mpr ha.symm]

Goal state after:
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))))
⊢ -↑π * I * ((1 + cexp (2 * ↑π * I * ↑z)) * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑z) ^ n) =
    ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
geom_series_mul_one_add
      (Complex.exp (2 * π * I * (z : ℂ))) (UpperHalfPlane.norm_exp_two_pi_I_lt_one _)

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 * (2 * ∑' (i : ℕ), cexp (2 * ↑π * I * ↑z) ^ i - 1) =
    ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑z) ^ n
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:
by
    rw [← summable_nat_add_iff 1] at this
    simpa using this

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

Goal state before:
pp: case hu
⊢ fibRec.IsSolution fun n ↦ ↑(Nat.fib n)

Tactic:
exact fib_isSol_fibRec

Goal state after:
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x ↦ (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))
B : Tendsto (fun x ↦ (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))
⊢ ∀ᶠ (a : ℕ) in atTop, u (n * a + r) / ↑(n * a + r) < L

Tactic:
refine ((B.comp tendsto_natCast_atTop_atTop).eventually (gt_mem_nhds hL)).mono fun k hk => ?_

Goal state after:
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x ↦ (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))
B : Tendsto (fun x ↦ (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))
k : ℕ
hk : ((fun x ↦ (x * u n + u r) / (x * ↑n + ↑r)) ∘ Nat.cast) k < L
⊢ u (n * k + r) / ↑(n * k + r) < L
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
⊢ ∀ᶠ (p : ℕ) in atTop, u p / ↑p < L

Tactic:
by
  /- It suffices to prove the statement for each arithmetic progression `(n * · + r)`. -/
  refine .atTop_of_arithmetic hn fun r _ => ?_
  /- `(k * u n + u r) / (k * n + r)` tends to `u n / n < L`, hence
  `(k * u n + u r) / (k * n + r) < L` for sufficiently large `k`. -/
  have A : Tendsto (fun x : ℝ => (u n + u r / x) / (n + r / x)) atTop (𝓝 ((u n + 0) / (n + 0))) :=
    (tendsto_const_nhds.add <| tendsto_const_nhds.div_atTop tendsto_id).div
      (tendsto_const_nhds.add <| tendsto_const_nhds.div_atTop tendsto_id) <| by simpa
  have B : Tendsto (fun x => (x * u n + u r) / (x * n + r)) atTop (𝓝 (u n / n)) := by
    rw [add_zero, add_zero] at A
    refine A.congr' <| (eventually_ne_atTop 0).mono fun x hx => ?_
    simp only [add_div' _ _ _ hx, div_div_div_cancel_right₀ hx, mul_comm]
  refine ((B.comp tendsto_natCast_atTop_atTop).eventually (gt_mem_nhds hL)).mono fun k hk => ?_
  /- Finally, we use an upper estimate on `u (k * n + r)` to get an estimate on
  `u (k * n + r) / (k * n + r)`. -/
  rw [mul_comm]
  refine lt_of_le_of_lt ?_ hk
  simp only [(· ∘ ·), ← Nat.cast_add, ← Nat.cast_mul]
  gcongr
  apply h.apply_mul_add_le

Goal state after:
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: case refine_1
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n ↦ u n / ↑n)
l : ℝ
hl : l < h.lim
⊢ ∀ᶠ (b : ℕ) in atTop, l < u b / ↑b

pp: case refine_2
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n ↦ u n / ↑n)
L : ℝ
hL : L > h.lim
⊢ ∀ᶠ (b : ℕ) in atTop, u b / ↑b < L

Tactic:
· refine eventually_atTop.2
      ⟨1, fun n hn => hl.trans_le (h.lim_le_div hbdd (zero_lt_one.trans_le hn).ne')⟩

Goal state after:
case refine_2
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n ↦ u n / ↑n)
L : ℝ
hL : L > h.lim
⊢ ∀ᶠ (b : ℕ) in atTop, u b / ↑b < L
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ x ∈ Finset.range (b - a), f ↑(a + x + 1) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x

Tactic:
add_assoc

Goal state after:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ x ∈ Finset.range (b - a), f ↑(a + (x + 1)) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsColimit
    ((CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯).map
      ShortComplex.π₂)

pp: case h₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsColimit
    ((CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯).map
      ShortComplex.π₃)

Tactic:
· exact isColimit f g

Goal state after:
case h₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsColimit
    ((CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯).map
      ShortComplex.π₃)
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case h.hb
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ 0 < ↑⌊c ^ i⌋₊ ^ 2

pp: case h.hd
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ 0 < (c ^ i) ^ 2

pp: case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ 1 * (c ^ i) ^ 2 ≤ (1 - c⁻¹)⁻¹ ^ 2 * ↑⌊c ^ i⌋₊ ^ 2

Tactic:
· apply sq_pos_of_pos
        refine zero_lt_one.trans_le ?_
        simp only [Nat.le_floor, one_le_pow₀, hc.le, Nat.one_le_cast, Nat.cast_one]

Goal state after:
case h.hd
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ 0 < (c ^ i) ^ 2

case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ 1 * (c ^ i) ^ 2 ≤ (1 - c⁻¹)⁻¹ ^ 2 * ↑⌊c ^ i⌋₊ ^ 2
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : L.Initial
⊢ (fst L R).Initial

Tactic:
have := L.initial_iff_isCofiltered_costructuredArrow.mp inferInstance
  exact initial_fst_of_isCofiltered_costructuredArrow L R

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Indization.LocallySmall

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : ObjectProperty.FullSubcategory IsIndObject
P : IndObjectPresentation X.obj
Q : IndObjectPresentation Y.obj
⊢ Small.{v, max u v} (X ⟶ Y)

Tactic:
let e₁ := IsColimit.coconePointUniqueUpToIso (P.isColimit) (colimit.isColimit _)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : ObjectProperty.FullSubcategory IsIndObject
P : IndObjectPresentation X.obj
Q : IndObjectPresentation Y.obj
e₁ : { pt := X.obj, ι := P.ι }.pt ≅ (colimit.cocone (P.F ⋙ yoneda)).pt :=
  P.isColimit.coconePointUniqueUpToIso (colimit.isColimit (P.F ⋙ yoneda))
⊢ Small.{v, max u v} (X ⟶ Y)
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
α : Type u_1
I : α → Type u_2
inst✝³ : (i : α) → Category.{v_1, u_2} (I i)
inst✝² : HasProductsOfShape α C
F : (i : α) → I i ⥤ C
inst✝¹ : ∀ (i : α), HasColimit (F i)
inst✝ : HasColimit (pointwiseProduct F)
k : (i : α) → I i
s : α
⊢ colimit.ι (pointwiseProduct F) k ≫ colimitPointwiseProductToProductColimit F ≫ Pi.π (fun s ↦ colimit (F s)) s =
    Pi.π ((Functor.pi F).obj k) s ≫ colimit.ι (F s) (k s)

Tactic:
simp [colimitPointwiseProductToProductColimit, Functor.pi, Pi.functor]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this : (F C).Faithful
⊢ (F C ⋙ G C ⋙ H C).Faithful

Tactic:
have : (G C).Faithful := by rw [G]; infer_instance

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this✝ : (F C).Faithful
this : (G C).Faithful
⊢ (F C ⋙ G C ⋙ H C).Faithful
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected

Goal state before:
pp: J : Type w
inst✝⁵ : Category.{w', w} J
inst✝⁴ : IsConnected J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPullbacks C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X : C
f : X ⟶ c.pt
hpull :
  IsPullback (colim.map (pullback.fst c.ι ((Functor.const J).map f)))
    (colim.map (pullback.snd c.ι ((Functor.const J).map f))) (colim.map c.ι) (colim.map ((Functor.const J).map f))
⊢ IsIso (colimMap (pullback.snd c.ι ((Functor.const J).map f)))

Tactic:
dsimp only [colim_obj, colim_map] at hpull

Goal state after:
J : Type w
inst✝⁵ : Category.{w', w} J
inst✝⁴ : IsConnected J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPullbacks C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X : C
f : X ⟶ c.pt
hpull :
  IsPullback (colimMap (pullback.fst c.ι ((Functor.const J).map f)))
    (colimMap (pullback.snd c.ι ((Functor.const J).map f))) (colimMap c.ι) (colimMap ((Functor.const J).map f))
⊢ IsIso (colimMap (pullback.snd c.ι ((Functor.const J).map f)))