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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), 0 < t → IntervalIntegrable g volume 0 t
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))

Tactic:
have key := lintegral_comp_eq_lintegral_meas_le_mul μ f_nn f_mble g_intble g_nn

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), 0 < t → IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:

Tactic:
_ = ‖(↑l ^ 2 - (s - ↑l) ^ 2) / ((s - ↑l) ^ 2 * ↑l ^ 2)‖ := by
      rw [div_sub_div, one_mul, mul_one]
      · simpa [sub_eq_zero]
      · simpa
    _ = ‖l ^ 2 - (s - l) ^ 2‖ / (‖s - l‖ ^ 2 * ‖l‖ ^ 2) := by simp
    _ ≤ ‖l ^ 2 - (s - l) ^ 2‖ / ((‖l‖ / 2) ^ 2 * ‖l‖ ^ 2) := by
      gcongr
      rw [norm_sub_rev]
      exact .trans (by linarith) (norm_sub_norm_le l s)
    _ = ‖s * (2 * l - s)‖ / (‖l‖ ^ 4 / 4) := by
      congr 1
      · rw [sq_sub_sq]; simp [← sub_add, two_mul, sub_add_eq_add_sub]
      · ring
    _ = (‖s‖ * ‖2 * l - s‖) / (‖l‖ ^ 4 / 4) := by simp
    _ = (4 * ‖s‖ * ‖2 * l - s‖) / ‖l‖ ^ 4 := by field
    _ ≤ (4 * r * (2.5 * ‖l‖)) / ‖l‖ ^ 4 := by
      gcongr (4 * ?_ * ?_) / ‖l‖ ^ 4
      refine (norm_sub_le _ _).trans ?_
      simp only [Complex.norm_mul, Complex.norm_ofNat]
      linarith
    _ = 10 * r / ‖l‖ ^ 3 := by field
    _ = _ := by norm_cast

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

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

Tactic:
by
  constructor
  · rintro ⟨x, rfl⟩
    rw [nthRoot_pow hn]
  · grind

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

Goal state before:
pp: a b : Multiset ℂ
h : a.card = b.card + 1
⊢ 1 ≤ (regularizedHGFunSeries a b).radius

Tactic:
by_cases! h' : ∀ j ∈ a, ∀ k : ℕ, j ≠ -k

Goal state after:
case pos
a b : Multiset ℂ
h : a.card = b.card + 1
h' : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
⊢ 1 ≤ (regularizedHGFunSeries a b).radius

case neg
a b : Multiset ℂ
h : a.card = b.card + 1
h' : ∃ j ∈ a, ∃ k, j = -↑k
⊢ 1 ≤ (regularizedHGFunSeries a b).radius
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: case one
θ : ℂ
⊢ eval (cos θ) (U ℂ 1) * sin θ = sin ((↑1 + 1) * θ)

Tactic:
simp [one_add_one_eq_two, sin_two_mul]

Goal state after:
case one
θ : ℂ
⊢ 2 * cos θ * sin θ = 2 * sin θ * cos θ
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
⊢ deriv ℘[L] x = ℘'[L] x

Tactic:
← L.weierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice,

Goal state after:
case neg
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
⊢ deriv ℘[L - L.ω₁ / 2] x = ℘'[L] x
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case refine_2
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
this :
  HasSum (fun i ↦ (1 / (2 * ↑(n + 1) + 1)) ^ 2 * ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ i)
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 * (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)⁻¹)
⊢ HasSum (fun k ↦ ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))

pp: case refine_1
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
⊢ (1 / (2 * ↑(n + 1) + 1)) ^ 2 < 1

Tactic:
· simp_rw [← _root_.pow_succ'] at this
      exact this

Goal state after:
case refine_1
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
⊢ (1 / (2 * ↑(n + 1) + 1)) ^ 2 < 1
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∉ L.lattice
⊢ (FormalMultilinearSeries.ofScalars ℂ fun i ↦
          if i = 0 then ℘[L - l₀] x else (↑i + 1) * (L.sumInvPow x (i + 2) - 0)).coeff
      (i + 1) =
    ∑' (l : ↥L.lattice),
      if ↑l = l₀ then 0 else (↑(i + 1) + 1) * (↑l - x) ^ (-↑(i + 1 + 2)) - Nat.casesOn (i + 1) (↑l ^ (-2)) 0

Tactic:
have h₁ (l : L.lattice) : l.1 ≠ l₀ := fun e ↦ hl₀ (e ▸ l.2)

Goal state after:
case neg
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∉ L.lattice
h₁ : ∀ (l : ↥L.lattice), ↑l ≠ l₀
⊢ (FormalMultilinearSeries.ofScalars ℂ fun i ↦
          if i = 0 then ℘[L - l₀] x else (↑i + 1) * (L.sumInvPow x (i + 2) - 0)).coeff
      (i + 1) =
    ∑' (l : ↥L.lattice),
      if ↑l = l₀ then 0 else (↑(i + 1) + 1) * (↑l - x) ^ (-↑(i + 1 + 2)) - Nat.casesOn (i + 1) (↑l ^ (-2)) 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
⊢ ↑↑(-k).negOnePow = (-1) ^ k

Tactic:
← Int.cast_negOnePow

Goal state after:
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
⊢ ↑↑(-k).negOnePow = ↑↑k.negOnePow
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
k : ℤ
hk : 2 * cos (↑r * π) = ↑k
hk_values : k ∈ Finset.Icc (-2) 2
⊢ ↑k / 2 ∈ {-1, -1 / 2, 0, 1 / 2, 1}

Tactic:
fin_cases hk_values

Goal state after:
case «0»
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hk : 2 * cos (↑r * π) = ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 0)
⊢ ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 0) / 2 ∈ {-1, -1 / 2, 0, 1 / 2, 1}

case «1»
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hk : 2 * cos (↑r * π) = ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 1)
⊢ ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 1) / 2 ∈ {-1, -1 / 2, 0, 1 / 2, 1}

case «2»
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hk : 2 * cos (↑r * π) = ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 2)
⊢ ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 2) / 2 ∈ {-1, -1 / 2, 0, 1 / 2, 1}

case «3»
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hk : 2 * cos (↑r * π) = ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 3)
⊢ ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 3) / 2 ∈ {-1, -1 / 2, 0, 1 / 2, 1}

case «4»
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hk : 2 * cos (↑r * π) = ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 4)
⊢ ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 4) / 2 ∈ {-1, -1 / 2, 0, 1 / 2, 1}
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
⊢ 0 < r z

Tactic:
by
  simp only [r, lt_min_iff, im_pos, Real.sqrt_pos, r1_pos, and_self]

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

Goal state before:
pp: n : ℤ
x : ℝ
hx : x ≤ -1
⊢ 1 ≤ ↑↑n.negOnePow * (↑↑n.negOnePow * eval (-x) (T ℝ n))

Tactic:
convert! one_le_eval_T_real n (le_neg_of_le_neg hx)

Goal state after:
n : ℤ
x : ℝ
hx : x ≤ -1
⊢ ↑↑n.negOnePow * (↑↑n.negOnePow * eval (-x) (T ℝ n)) = eval (-x) (T ℝ n)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case refine_1
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
this : AnalyticAt ℂ ℘[L - l₀] l₀
⊢ AnalyticAt ℂ (fun z ↦ (z - l₀) ^ 2 / l₀ ^ 2) l₀

Tactic:
by_cases hl₀ : l₀ = 0

Goal state after:
case pos
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
this : AnalyticAt ℂ ℘[L - l₀] l₀
hl₀ : l₀ = 0
⊢ AnalyticAt ℂ (fun z ↦ (z - l₀) ^ 2 / l₀ ^ 2) l₀

case neg
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
this : AnalyticAt ℂ ℘[L - l₀] l₀
hl₀ : ¬l₀ = 0
⊢ AnalyticAt ℂ (fun z ↦ (z - l₀) ^ 2 / l₀ ^ 2) l₀
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case e'_4
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] (T ℝ ↑n)) = sumNodes n (fun i ↦ iterateDerivativeC n k x i) (T ℝ ↑n)

Tactic:
rw [sumNodes_eq_eval_iterate_derivative hk x (le_of_eq (degree_T ℝ n))]

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

Goal state before:
pp: z : ℂ
c₁ c₂ : ℤ
⊢ Summable fun n ↦ ((↑c₁ * z - ↑n) * (↑c₂ * z + ↑n))⁻¹

Tactic:
apply summable_inv_of_isBigO_rpow_inv (a := 2) (by norm_cast)

Goal state after:
z : ℂ
c₁ c₂ : ℤ
⊢ (fun n ↦ ((↑c₁ * z - ↑n) * (↑c₂ * z + ↑n))⁻¹) =O[cofinite] fun n ↦ (|↑n| ^ 2)⁻¹
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℂ
c₁ c₂ : ℤ
⊢ Summable fun n ↦ ((↑c₁ * z + ↑n + 1) * (↑c₂ * z + ↑n))⁻¹

Tactic:
apply summable_inv_of_isBigO_rpow_inv (a := 2) (by norm_cast)

Goal state after:
z : ℂ
c₁ c₂ : ℤ
⊢ (fun n ↦ ((↑c₁ * z + ↑n + 1) * (↑c₂ * z + ↑n))⁻¹) =O[cofinite] fun n ↦ (|↑n| ^ 2)⁻¹
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℂ
hz : z ≠ 0
c₁ c₂ : ℤ
⊢ Summable fun n ↦ ((↑n * z + ↑c₁) * (↑n * z + ↑c₂))⁻¹

Tactic:
apply summable_inv_of_isBigO_rpow_inv (a := 2) (by norm_cast)

Goal state after:
z : ℂ
hz : z ≠ 0
c₁ c₂ : ℤ
⊢ (fun n ↦ ((↑n * z + ↑c₁) * (↑n * z + ↑c₂))⁻¹) =O[cofinite] fun n ↦ (|↑n| ^ 2)⁻¹
Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f : ι → 𝕜 → F
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
hf : ∀ y ∈ s, Summable fun n ↦ f n y
h : SummableLocallyUniformlyOn (fun n ↦ derivWithin (fun z ↦ f n z) s) s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt 𝕜 (f n) r
⊢ derivWithin (fun z ↦ ∑' (n : ι), f n z) s x = ∑' (n : ι), derivWithin (f n) s x

Tactic:
apply HasDerivWithinAt.derivWithin ?_ (hs.uniqueDiffWithinAt hx)
  apply HasDerivAt.hasDerivWithinAt
  apply hasDerivAt_of_tendstoLocallyUniformlyOn hs _ _ (fun y hy ↦ (hf y hy).hasSum) hx
    (f' := fun n : Finset ι ↦ fun a ↦ ∑ i ∈ n, derivWithin (fun z ↦ f i z) s a)
  · obtain ⟨g, hg⟩ := h
    apply (hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn.mp hg).congr_right
    exact fun _ hb ↦ (hg.tsum_eqOn hb).symm
  · filter_upwards with t r hr using HasDerivAt.fun_sum
      (fun q hq ↦ ((hf2 q r hr).differentiableWithinAt.hasDerivWithinAt.hasDerivAt)
      (hs.mem_nhds hr))

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

Goal state before:
pp: L : PeriodPair
this : 7 ≤ meromorphicOrderAt (L.relation * id ^ 6) 0
⊢ 1 ≤ meromorphicOrderAt L.relation 0

Tactic:
rw [meromorphicOrderAt_mul (by fun_prop) (by fun_prop),
      meromorphicOrderAt_pow (by fun_prop)] at this

Goal state after:
L : PeriodPair
this : 7 ≤ meromorphicOrderAt L.relation 0 + ↑6 * meromorphicOrderAt id 0
⊢ 1 ≤ meromorphicOrderAt L.relation 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
⊢ Multipliable fun i ↦ 1 + sineTerm x i

Tactic:
apply multipliable_one_add_of_summable

Goal state after:
x : ℂ
⊢ Summable fun i ↦ ‖sineTerm x i‖
Module: Mathlib.Tactic.NormNum.Prime

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

Tactic:
refine ⟨Nat.lt_add_right _ h.1, ?_, ?_⟩

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

case refine_2
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
⊢ k + 2 ≤ n.minFac
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:
refine minFacHelper_1 e h fun h2 ↦ ?_
  rw [← h2] at nk
  exact nk <| minFac_prime h.one_lt.ne'

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

Goal state before:
pp: α : Type u_1
inst✝ : CommSemiring α
n : ℕ
⊢ ↑(Nat.fib (n + 2)) = ∑ x, ![1, 1] x * ↑(Nat.fib (n + ↑x))

Tactic:
rw [Nat.fib_add_two, add_comm]

Goal state after:
α : Type u_1
inst✝ : CommSemiring α
n : ℕ
⊢ ↑(Nat.fib (n + 1) + Nat.fib n) = ∑ x, ![1, 1] x * ↑(Nat.fib (n + ↑x))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case h₂
k : ℕ
K : Set ℂ
A B : ℝ
hB : 0 < B
hKAB : K ⊆ UpperHalfPlane.coe '' verticalStrip A B
n : ℕ
a : ℍ
haAB : a ∈ verticalStrip A B
ha : ↑a ∈ K
h1 :
  ‖↑(![1, ↑n + 1] 0) * ↑a + ↑(![1, ↑n + 1] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * ‖![1, ↑n + 1]‖ ^ (-(↑k + 1))
h2 :
  ‖↑(![1, -(↑n + 1)] 0) * ↑a + ↑(![1, -(↑n + 1)] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * (↑n + 1) ^ (-(↑k + 1))
⊢ ‖(↑a - (↑n + 1)) ^ (-1 - ↑k)‖ ≤ r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-1 - ↑k) * |↑n + 1| ^ (-1 - ↑k)

Tactic:
· simpa (disch := positivity) [sub_eq_add_neg, ← Real.rpow_intCast, abs_norm_eq_max_natAbs,
      abs_of_nonneg] using h2

Goal state after:
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k M : ℕ
c : ℝ
hc : 0 < c
i : ℕ
| rexp (log 2) ^ (-(c * ↑i))

Tactic:
← exp_mul

Goal state after:
k M : ℕ
c : ℝ
hc : 0 < c
i : ℕ
| rexp (log 2 * -(c * ↑i))
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
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun x ↦ u (c x) / ↑(c x) - l) atTop (𝓝 0)
⊢ ∀ᶠ (n : ℕ) in atTop, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)

Tactic:
← Asymptotics.isLittleO_one_iff ℝ,

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
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : (fun x ↦ u (c x) / ↑(c x) - l) =o[atTop] fun _x ↦ 1
⊢ ∀ᶠ (n : ℕ) in atTop, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)
Module: Mathlib.Analysis.VonNeumannAlgebra.Basic

Goal state before:
pp: H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
e : H →L[ℂ] H
he : IsStarProjection e
S : VonNeumannAlgebra H
⊢ ((∀ x ∈ S.commutant, e ∘SL x ∘SL e = x ∘SL e) ∧ ∀ x ∈ S.commutant, e ∘SL x ∘SL e = e ∘SL x) ↔
    ∀ x ∈ S.commutant, e ∘SL x ∘SL e = x ∘SL e

Tactic:
and_iff_left_iff_imp,

Goal state after:
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
e : H →L[ℂ] H
he : IsStarProjection e
S : VonNeumannAlgebra H
⊢ (∀ x ∈ S.commutant, e ∘SL x ∘SL e = x ∘SL e) → ∀ x ∈ S.commutant, e ∘SL x ∘SL e = e ∘SL x
Module: Mathlib.Analysis.SumIntegralComparisons

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

Tactic:
suffices ∫ x in a..a + ↑(b - a), f x ≤ ∑ x ∈ .Ico (0 + a) (b - a + a), f x by simp_all
  rw [← Finset.sum_Ico_add, Nat.Ico_zero_eq_range]
  suffices ∫ x in a..a + ↑(b - a), f x ≤ ∑ x ∈ .range (b - a), f (a + x) by simp_all
  exact AntitoneOn.integral_le_sum (by simp only [hf, hab, Nat.cast_sub, add_sub_cancel])

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k : A ⟶ X ⊞ Y
hk : k ≫ φ f g = 0
⊢ (k ≫ biprod.fst) ≫ f ≫ g = 0

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k : A ⟶ X ⊞ Y
hk : k ≫ φ f g = 0
⊢ kernel.lift (f ≫ g) (k ≫ biprod.fst) ?refine_1 ≫ ι f g = k

Tactic:
all_goals
      obtain ⟨k₁, k₂, rfl⟩ := biprod.decomp_hom_to k
      simp only [biprod.ext_to_iff, add_comp, assoc, inl_φ, BinaryBicone.inl_fst,
        comp_id, inr_φ_fst, comp_neg, zero_comp, BinaryBicone.inl_snd, comp_zero, φ_snd,
        BinaryBicone.inr_snd_assoc, zero_add, add_neg_eq_zero] at hk
      obtain ⟨rfl, hk⟩ := hk
      aesop

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
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun x ↦ u (c x) / ↑(c x) - l) atTop (𝓝 0)
⊢ ∀ᶠ (n : ℕ) in atTop, ↑(c n) * l - u (c n) ≤ ε * ↑(c n)

Tactic:
← Asymptotics.isLittleO_one_iff ℝ,

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
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : (fun x ↦ u (c x) / ↑(c x) - l) =o[atTop] fun _x ↦ 1
⊢ ∀ᶠ (n : ℕ) in atTop, ↑(c n) * l - u (c n) ≤ ε * ↑(c n)
Module: Mathlib.CategoryTheory.Abelian.Yoneda

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
D : Type u'
inst✝² : Category.{v', u'} D
F : D ⥤ C
inst✝¹ : F.Full
G : C
inst✝ : Projective G
hG : IsSeparator G
hG₂ : ∀ (X : D), ∃ p, Epi p
X Y : D
f : (F ⋙ preadditiveCoyonedaObj G).obj X ⟶ (F ⋙ preadditiveCoyonedaObj G).obj Y
p : G ⟶ F.obj X
h✝ : Epi p
⊢ ∃ a, (F ⋙ preadditiveCoyonedaObj G).map a = f

Tactic:
obtain ⟨f, rfl⟩ := preadditiveCoyonedaObj_map_surjective hG p f

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
D : Type u'
inst✝² : Category.{v', u'} D
F : D ⥤ C
inst✝¹ : F.Full
G : C
inst✝ : Projective G
hG : IsSeparator G
hG₂ : ∀ (X : D), ∃ p, Epi p
X Y : D
p : G ⟶ F.obj X
h✝ : Epi p
f : F.obj X ⟶ F.obj Y
⊢ ∃ a, (F ⋙ preadditiveCoyonedaObj G).map a = (preadditiveCoyonedaObj G).map f
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case hab
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
⊢ (c⁻¹ ^ 2) ^ ↑⌊Real.log j / Real.log c⌋₊ ≤ (c⁻¹ ^ 2) ^ (Real.log j / Real.log c - 1)

Tactic:
exact Real.rpow_le_rpow_of_exponent_ge A C.le (Nat.sub_one_lt_floor _).le

Goal state after:
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)
h₁ :
  (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙
      inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
h₂ : (inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final
c : Cocone (inclusion (fromFinalModel (CostructuredArrow yoneda A)) ⋙ CostructuredArrow.proj yoneda A ⋙ yoneda) :=
  Cocone.whisker (inclusion (fromFinalModel (CostructuredArrow yoneda A))) (Presheaf.tautologicalCocone A)
hc : IsColimit c :=
  (Functor.Final.isColimitWhiskerEquiv (inclusion (fromFinalModel (CostructuredArrow yoneda A)))
        (Presheaf.tautologicalCocone A)).symm
    (Presheaf.isColimitTautologicalCocone A)
hq : Nonempty (FinalModel (CostructuredArrow yoneda A))
⊢ IsIndObject A

Tactic:
exact ⟨_, inclusion (fromFinalModel _) ⋙ CostructuredArrow.proj yoneda A, c.ι, hc⟩

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
h : IsZero (Ψ.r.obj (Φ.quotient.obj X))
⊢ (Φ.colon Ψ).ι.app X ≫ Φ.π.app X = 0

Tactic:
rw [colon_ι_app_π_app, h.eq_zero_of_tgt ((colonπ Φ Ψ).app X), zero_comp]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
a : Pseudoelement P
x : Over P
⊢ (fun g_1 ↦ app (f ≫ g) g_1) x ≈ (fun g_1 ↦ app g g_1) ((fun g ↦ app f g) x)

Tactic:
by
      simp only [app]
      rw [← Category.assoc, Over.coe_hom]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Surjective (pseudoApply f)
pbar : Pseudoelement P
hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
p : Over P
hp : ⟦p⟧ = pbar
this : ⟦Over.mk (p.hom ≫ f)⟧ = ⟦Over.mk (𝟙 Q)⟧
⊢ Epi f

Tactic:
have ⟨R, x, y, _, ey, comm⟩ := Quotient.exact this

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Surjective (pseudoApply f)
pbar : Pseudoelement P
hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
p : Over P
hp : ⟦p⟧ = pbar
this : ⟦Over.mk (p.hom ≫ f)⟧ = ⟦Over.mk (𝟙 Q)⟧
R : C
x : R ⟶ (Over.mk (p.hom ≫ f)).left
y : R ⟶ (Over.mk (𝟙 Q)).left
w✝ : Epi x
ey : Epi y
comm : x ≫ (Over.mk (p.hom ≫ f)).hom = y ≫ (Over.mk (𝟙 Q)).hom
⊢ Epi f
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
inst✝ : HasDerivedCategory C
x : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) ↑n
⊢ (R.extEquivCohomologyClass.symm (CohomologyClass.mk x)).hom =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
      ((ShiftedHom.map (Cocycle.equivHomShift.symm x) DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯)
      ⋯

Tactic:
by
  change SmallShiftedHom.equiv _ _ (.comp _ (CohomologyClass.mk x).toSmallShiftedHom _) = _
  simp only [SmallShiftedHom.equiv_comp, SmallShiftedHom.equiv_mk₀Inv, isoOfHom, asIso_inv,
    CohomologyClass.equiv_toSmallShiftedHom_mk,
    DerivedCategory.singleFunctorIsoCompQ, Iso.refl_hom, NatTrans.id_app, Category.id_comp,
    Iso.refl_inv]
  congr
  exact (ShiftedHom.comp_mk₀_id ..).symm

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝⁵ : P.IsSerreClass
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
this : HasFiniteProducts D
⊢ Abelian D

Tactic:
have := hasKernels L P

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝⁵ : P.IsSerreClass
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
this✝ : HasFiniteProducts D
this : HasKernels D
⊢ Abelian D
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.Monoidal
⊢ ε F ≫ η F = 𝟙 (𝟙_ W)

Tactic:
ε_η

Goal state after:
V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.Monoidal
⊢ 𝟙 (𝟙_ W) = 𝟙 (𝟙_ W)