mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: r : ℝ
f : ℕ → ℝ
⊢ (∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun n ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun n ↦ i.2) ↔
    (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s

Tactic:
refine ⟨fun H ↦ ⟨fun s hs ↦ ?_, fun s hs ↦ ?_⟩, fun H ⟨s, t⟩ ⟨hs, ht⟩ ↦ ⟨?_, ?_⟩⟩

Goal state after:
case refine_1
r : ℝ
f : ℕ → ℝ
H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun n ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun n ↦ i.2
s : ℝ
hs : s < r
⊢ ↑s ≤ ofSeq f

case refine_2
r : ℝ
f : ℕ → ℝ
H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun n ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun n ↦ i.2
s : ℝ
hs : s > r
⊢ ofSeq f ≤ ↑s

case refine_3
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s
x✝¹ : ℝ × ℝ
s t : ℝ
x✝ : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
⊢ (ofSeq fun n ↦ (s, t).1) < ofSeq f

case refine_4
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, ↑s ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ ↑s
x✝¹ : ℝ × ℝ
s t : ℝ
x✝ : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
⊢ ofSeq f < ofSeq fun n ↦ (s, t).2
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: ⊢ ↑3 ≤ π + 1 / 2

Tactic:
grind [pi_gt_three]

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

Goal state before:
pp: x : ℝ
m : ℤ
h : Irrational (x * ↑m)
⊢ Irrational (x * ↑↑m)

Tactic:
rwa [cast_intCast]

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

Goal state before:
pp: x : ℝ
m : ℤ
h : Irrational (↑m * x)
⊢ Irrational (↑↑m * x)

Tactic:
rwa [cast_intCast]

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

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ (rexp (log (x + √(x ^ 2 - 1))) + rexp (-log (x + √(x ^ 2 - 1)))) / 2 = x

Tactic:
exp_neg,

Goal state after:
x : ℝ
hx : 1 ≤ x
⊢ (rexp (log (x + √(x ^ 2 - 1))) + (rexp (log (x + √(x ^ 2 - 1))))⁻¹) / 2 = x
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ (rexp (log (x + √(x ^ 2 - 1))) - rexp (-log (x + √(x ^ 2 - 1)))) / 2 = √(x ^ 2 - 1)

Tactic:
exp_neg,

Goal state after:
x : ℝ
hx : 1 ≤ x
⊢ (rexp (log (x + √(x ^ 2 - 1))) - (rexp (log (x + √(x ^ 2 - 1))))⁻¹) / 2 = √(x ^ 2 - 1)
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
tendstoTop : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
⊢ ¬ContinuousAt (deriv (qaryEntropy q)) 0

Tactic:
apply not_continuousAt_of_tendsto (Filter.Tendsto.congr' _ tendstoTop) nhdsWithin_le_nhds

Goal state after:
q : ℕ
tendstoTop : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
⊢ Disjoint (𝓝 (deriv (qaryEntropy q) 0)) atTop

q : ℕ
tendstoTop : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
⊢ (fun p ↦ log (↑q - 1) + log (1 - p) - log p) =ᶠ[𝓝[>] 0] deriv (qaryEntropy q)
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: a : ℝ
x : ℕ
⊢ a * ((a ^ 2) ^ x / ↑x !) = a ^ (2 * x + 1) / ↑x !

Tactic:
rw [← pow_mul, mul_div_assoc', _root_.pow_succ']

Goal state after:
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
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ a ^ p

Tactic:
have hIcc : Icc (0 : ℝ≥0) 1 = Ioo 0 1 ∪ {0} ∪ {1} := by ext; simp
  rw [hIcc] at hp
  obtain (hp | hp) | hp := hp
  · exact concaveOn_nnrpow_Ioo hp
  · simp only [mem_singleton_iff] at hp
    simp only [hp, nnrpow_zero]
    exact concaveOn_const _ (convex_Ici _)
  · simp only [mem_singleton_iff] at hp
    simp only [hp]
    exact ConcaveOn.congr (concaveOn_id (convex_Ici _)) nnrpow_one_eqOn.symm

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
u : ℝ → E := fun x ↦ x⁻¹ • f x
hint : ∀ {p q : ℝ}, 0 < p → 0 < q → IntervalIntegrable u volume p q
ε r : ℝ
hε : 0 < ε
hr : 0 < r
⊢ (∫ (x : ℝ) in ε..r, x⁻¹ • f (a * x)) - ∫ (x : ℝ) in ε..r, x⁻¹ • f (b * x) =
    (∫ (y : ℝ) in a * ε..a * r, u y) - ∫ (y : ℝ) in b * ε..b * r, u y

Tactic:
by
        rw [integral_comp_mul_inv_smul ha.ne', integral_comp_mul_inv_smul hb.ne']

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

Goal state before:
pp: this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 1 / 2 < eulerMascheroniSeq 6

Tactic:
rw [this, lt_sub_iff_add_lt, ← lt_sub_iff_add_lt', log_lt_iff_lt_exp (by positivity)]

Goal state after:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 7 < rexp (49 / 20 - 1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h1 : s.Gammaℝ ≠ 0
h2 : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
⊢ (1 - s).Gammaℝ⁻¹ = s.Gammaℂ * cos (↑π * s / 2) * s.Gammaℝ⁻¹

Tactic:
← Gammaℝ_div_Gammaℝ_one_sub h2,

Goal state after:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h1 : s.Gammaℝ ≠ 0
h2 : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
⊢ (1 - s).Gammaℝ⁻¹ = s.Gammaℝ / (1 - s).Gammaℝ * s.Gammaℝ⁻¹
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: n : ℕ
⊢ deriv Gamma (↑n + 1) = ↑n ! * (-γ + ↑(harmonic n))

Tactic:
let f := log ∘ Gamma

Goal state after:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
⊢ deriv Gamma (↑n + 1) = ↑n ! * (-γ + ↑(harmonic n))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 0 1
C : ℝ≥0 := NNReal.mk (∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1)⁻¹ ⋯
⊢ ∃ μ,
    ∀ x ∈ Ici 0,
      IntegrableOn (fun t ↦ p.rpowIntegrand₀₁ t x) (Ioi 0) μ ∧ x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x ∂μ

Tactic:
refine ⟨C • volume, fun x hx => ⟨?_, ?_⟩⟩

Goal state after:
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)

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.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: case hd
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ (fun s ↦ 2 ^ (1 - 2 * s)) (1 / 2)

Tactic:
· exact DifferentiableAt.rpow (by fun_prop) (by fun_prop) two_ne_zero

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

Goal state before:
pp: case refine_1
m : ℕ
⊢ ¬1 / 2 = -↑m

Tactic:
exact ((neg_nonpos.mpr m.cast_nonneg).trans_lt one_half_pos).ne'

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
hy : 0 < y
⊢ log y < log x ↔ y < x

Tactic:
exact log_lt_log_iff hy hx

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

Goal state before:
pp: x : ℝ
⊢ x ≤ 1 / rexp (-(x * x))

Tactic:
exp_neg,

Goal state after:
x : ℝ
⊢ x ≤ 1 / (rexp (x * x))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone

Goal state before:
pp: a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
x✝ : y ∈ Ici (rexp a⁻¹)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ log y / y ^ a ≤ log x / x ^ a

Tactic:
← rpow_one y,

Goal state after:
a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
x✝ : y ∈ Ici (rexp a⁻¹)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ log (y ^ 1) / y ^ a ≤ log x / x ^ a
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε✝ : ℝ≥0∞
hε✝ : 0 < ε✝
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
a✝ : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
n : ℕ
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ m, P (⋂ m', ⋂ (_ : m' ≤ m), (f n m')ᶜ) < ε

Tactic:
refine exists_measure_iInter_lt (fun m ↦ ?_) hε ⟨0, measure_ne_top P _⟩ ?_

Goal state after:
case refine_1
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε✝ : ℝ≥0∞
hε✝ : 0 < ε✝
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
a✝ : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
n : ℕ
ε : ℝ≥0∞
hε : 0 < ε
m : ℕ
⊢ NullMeasurableSet (f n m)ᶜ P

case refine_2
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε✝ : ℝ≥0∞
hε✝ : 0 < ε✝
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
a✝ : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
n : ℕ
ε : ℝ≥0∞
hε : 0 < ε
⊢ ⋂ n_1, (f n n_1)ᶜ = ∅
Module: Mathlib.Analysis.SpecialFunctions.Pochhammer

Goal state before:
pp: k n : ℕ
⊢ ↑k < ↑n - 1 → k < n

Tactic:
← @Nat.cast_lt ℝ

Goal state after:
k n : ℕ
⊢ ↑k < ↑n - 1 → ↑k < ↑n
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 : ℂ
h₁ : x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ
h₂ : x + ↑l ∈ ↑L.lattice
h₃ : x + ↑l ≠ l₀
⊢ x ∈ ↑L.lattice

Tactic:
simpa using sub_mem h₂ l.2

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

Goal state before:
pp: L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
⊢ ℘[L] (z + ↑l) = ℘[L] z

Tactic:
by_cases hz : z ∈ L.lattice

Goal state after:
case pos
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∈ L.lattice
⊢ ℘[L] (z + ↑l) = ℘[L] z

case neg
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∉ L.lattice
⊢ ℘[L] (z + ↑l) = ℘[L] z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: x : ℝ
h : x ≠ -1
⊢ HasDerivWithinAt arcsin (1 / √(1 - x ^ 2)) (Ici x) x

Tactic:
by
  rcases eq_or_ne x 1 with (rfl | h')
  · convert! (hasDerivWithinAt_const (1 : ℝ) _ (π / 2)).congr _ _ <;>
      simp +contextual [arcsin_of_one_le]
  · exact (hasDerivAt_arcsin h h').hasDerivWithinAt

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

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
⊢ √(2 * π * ↑n) * (↑n / rexp 1) ^ n ≤ ↑n !

Tactic:
have : √(2 * π * n) * (n / exp 1) ^ n = √π * (√(2 * n) * (n / exp 1) ^ n) := by
    simp [sqrt_mul']; ring

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
this : √(2 * π * ↑n) * (↑n / rexp 1) ^ n = √π * (√(2 * ↑n) * (↑n / rexp 1) ^ n)
⊢ √(2 * π * ↑n) * (↑n / rexp 1) ^ n ≤ ↑n !
Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn

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

Tactic:
apply HasSumLocallyUniformlyOn.summableLocallyUniformlyOn (g := fun x ↦ ∑' n, f n x)

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : CompleteSpace F
inst✝¹ : TopologicalSpace β
inst✝ : LocallyCompactSpace β
f : α → β → F
s : Set β
hs : IsOpen[inst✝¹] s
hu : ∀ K ⊆ s, IsCompact K → ∃ u, Summable u ∧ ∀ᶠ (n : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n
⊢ HasSumLocallyUniformlyOn f (fun x ↦ ∑' (n : α), f n x) s
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < ↑k + 1
key : ∫ (t : ℝ) in Ioi 0, t ^ (↑k + 1 - 1) * rexp (-(c * t)) = (1 / c) ^ (↑k + 1) * Gamma (↑k + 1)
hint : IntegrableOn (fun x ↦ x ^ (↑k + 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
⊢ ↑k ! * c⁻¹ ^ (↑k + 1) = ↑k ! * (c ^ (k + 1))⁻¹

Tactic:
inv_rpow hc.le,

Goal state after:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < ↑k + 1
key : ∫ (t : ℝ) in Ioi 0, t ^ (↑k + 1 - 1) * rexp (-(c * t)) = (1 / c) ^ (↑k + 1) * Gamma (↑k + 1)
hint : IntegrableOn (fun x ↦ x ^ (↑k + 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
⊢ ↑k ! * (c ^ (↑k + 1))⁻¹ = ↑k ! * (c ^ (k + 1))⁻¹
Module: Mathlib.Analysis.SumIntegralComparisons

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

Tactic:
by
  rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]
  exact hf.neg.sum_le_integral_Ico hab

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
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
n : ℕ
hn : ↑n * l - u n ≤ ε * (1 + l) * ↑n
npos : n ∈ Set.Ioi 0
⊢ d < l - ε * (1 + l)

Tactic:
linarith only [hε]

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case refine_2
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 ℕ
⊢ ∑ i ∈ s, f ↑(i + N + 1) ≤ ∫ (x : ℝ) in Set.Ioi ↑N, f x

Tactic:
obtain ⟨t, ht⟩ := tendsto_finset_range.eventually (Ici_mem_atTop s) |>.exists
    calc
      ∑ i ∈ s, f ↑(i + N + 1) ≤ ∑ i ∈ range t, f ↑(i + N + 1) :=
        sum_le_sum_of_subset_of_nonneg ht <| by grind
      _ = ∑ i ∈ Ico N (N + t), f ↑(i + 1) := by rw [Finset.sum_Ico_eq_sum_range]; grind
      _ ≤ ∫ (x : ℝ) in Set.Ioi (N : ℝ), f x :=
        (anti.mono <| by grind).sum_Ico_le_integral integrable nonneg

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case base.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
x : α
⊢ FilteredClosureSmall.abstractFilteredClosureRealization f ⟨0, id { down := x }⟩ = { obj := f x, property := ⋯ }.obj

Tactic:
simp only [FilteredClosureSmall.abstractFilteredClosureRealization,
          FilteredClosureSmall.bundledAbstractFilteredClosure]
        rfl

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
T : Type u₃
inst✝⁴ : Category.{v₃, u₃} T
L : C ⥤ T
R : D ⥤ T
C' : Type u₄
inst✝³ : Category.{v₄, u₄} C'
D' : Type u₅
inst✝² : Category.{v₅, u₅} D'
T' : Type u₆
inst✝¹ : Category.{v₆, u₆} T'
L' : C' ⥤ T'
R' : D' ⥤ T'
F₁ : C ⥤ C'
F₂ : D ⥤ D'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝ : IsIso β
X : Comma L' R'
Y Z : Comma (map₂ (𝟙 (L'.obj X.left)) α) (map₂ X.hom (inv β))
f : Y ⟶ Z
⊢ (mk { left := Y.left.hom, right := Y.right.hom, w := ⋯ }).right.right ⟶
    (mk { left := Z.left.hom, right := Z.right.hom, w := ⋯ }).right.right

Tactic:
exact f.right.right

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
f g h : Over P
x✝¹ : PseudoEqual P f g
x✝ : PseudoEqual P g h
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
⊢ (pullback.fst q p' ≫ p) ≫ f.hom = (pullback.snd q p' ≫ q') ≫ h.hom

Tactic:
rw [Category.assoc, comm, ← Category.assoc, pullback.condition, Category.assoc, comm',
    Category.assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
a✝ : R
x✝ y✝ : X ⟶ Y
⊢ (a✝ • (x✝ + y✝)).hom = (a✝ • x✝ + a✝ • y✝).hom

Tactic:
exact smul_add _ _ _

Goal state after:
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
⊢ ∀ (a : R) (x y : X ⟶ Y), a • (x + y) = a • x + a • y

Tactic:
by intros; ext; exact smul_add _ _ _

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : LeftRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (F ⊗ { obj := fun X ↦ ᘁ(F.obj X), map := fun {X Y} f ↦ ᘁF.map (inv f), map_id := ⋯, map_comp := ⋯ }).map f ≫
      ε_ ({ obj := fun X ↦ ᘁ(F.obj X), map := fun {X Y} f ↦ ᘁF.map (inv f), map_id := ⋯, map_comp := ⋯ }.obj Y)
        (F.obj Y) =
    ε_ ({ obj := fun X ↦ ᘁ(F.obj X), map := fun {X Y} f ↦ ᘁF.map (inv f), map_id := ⋯, map_comp := ⋯ }.obj X)
        (F.obj X) ≫
      (𝟙_ (C ⥤ D)).map f

Tactic:
simp [tensorHom_def, leftAdjointMate_comp_evaluation]

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

Goal state before:
pp: case refine_1
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
F : C ⥤ₑ E
G : D ⥤ₑ E
e : (whiskeringLeft L P E).obj G ≅ F
⊢ P.isoModSerre.IsInvertedBy F.obj

Tactic:
← MorphismProperty.IsInvertedBy.iff_of_iso _
      (show L ⋙ G.obj ≅ F.obj from (ObjectProperty.ι _).mapIso e)

Goal state after:
case refine_1
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
F : C ⥤ₑ E
G : D ⥤ₑ E
e : (whiskeringLeft L P E).obj G ≅ F
⊢ P.isoModSerre.IsInvertedBy (L ⋙ G.obj)
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
⊢ R.IsRightAdjoint

Tactic:
let R' : A ⥤ _ := R ⋙ Monad.comparison (monadicAdjunction U)
  rsuffices : R'.IsRightAdjoint
  · let : (R' ⋙ (Monad.comparison (monadicAdjunction U)).inv).IsRightAdjoint := by
      infer_instance
    refine ((Adjunction.ofIsRightAdjoint
      (R' ⋙ (Monad.comparison (monadicAdjunction U)).inv)).ofNatIsoRight ?_).isRightAdjoint
    exact Functor.isoWhiskerLeft R (Monad.comparison _).asEquivalence.unitIso.symm ≪≫ R.rightUnitor
  let : (R' ⋙ Monad.forget (monadicAdjunction U).toMonad).IsRightAdjoint := by
    refine ((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight ?_).isRightAdjoint
    exact Functor.isoWhiskerLeft R (Monad.comparisonForget (monadicAdjunction U)).symm
  let : ∀ X, RegularEpi ((Monad.adj (monadicAdjunction U).toMonad).counit.app X) := by
    intro X
    simp only [Monad.adj_counit]
    exact ⟨_, _, _, _, Monad.beckAlgebraCoequalizer X⟩
  exact isRightAdjoint_triangle_lift R' (Monad.adj _) this

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Triple

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ (∀ (X : C), Mono (t.leftToRight.app X)) ↔ ∀ (X : D), Mono (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)

Tactic:
refine ⟨fun h X ↦ by rw [← leftToRight_app_obj]; exact h _, fun h X ↦ ?_⟩
  rw [mono_leftToRight_app_iff_mono_adj₂_unit_app]
  simpa using h (F.obj X)

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.End

Goal state before:
pp: C : Type u
inst✝ : Bicategory C
X : C
⊢ ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : X ⟶ X} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    ((fun {x x_1} η h ↦ η ▷ h) f₁ X₂ ≫ (fun {f x x_1} η ↦ f ◁ η) f₂) ≫
        (fun {x x_1} η h ↦ η ▷ h) g₁ Y₂ ≫ (fun {f x x_1} η ↦ f ◁ η) g₂ =
      (fun {x x_1} η h ↦ η ▷ h) (f₁ ≫ g₁) X₂ ≫ (fun {f x x_1} η ↦ f ◁ η) (f₂ ≫ g₂)

Tactic:
intros
    dsimp only
    rw [Bicategory.whiskerLeft_comp, Bicategory.comp_whiskerRight, Category.assoc, Category.assoc,
      Bicategory.whisker_exchange_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
W✝ X✝ Y✝ Z✝ : ∫ F
f : W✝ ⟶ X✝
g : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h

Tactic:
ext
    · simp
    · simp [mapComp_assoc_right_hom_app_assoc, Strict.associator_eqToIso]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a : B
F : LocallyDiscrete (Discrete Unit) ⥤ᵒᵖᴸ B
⊢ (F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫ F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } })) ≫
      MonoidalCategoryStruct.whiskerRight (F.mapId { as := { as := () } }) (F.map (𝟙 { as := { as := () } })) =
    (MonoidalCategoryStruct.leftUnitor (F.map (𝟙 { as := { as := () } }))).inv

Tactic:
simp only [tensorUnit_def, tensorObj_def, whiskerRight_def, Category.assoc, leftUnitor_def]

Goal state after:
B : Type u
inst✝ : Bicategory B
a : B
F : LocallyDiscrete (Discrete Unit) ⥤ᵒᵖᴸ B
⊢ F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫
      F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } }) ≫
        F.mapId { as := { as := () } } ▷ F.map (𝟙 { as := { as := () } }) =
    (λ_ (F.map (𝟙 { as := { as := () } }))).inv
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵒᵖᴸ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ F.mapComp' f₀₂ f₂₃ f ⋯ ≫ F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ =
    F.mapComp' f₀₁ f₁₃ f ⋯ ≫ F.map f₀₁ ◁ F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv

Tactic:
rw [F.mapComp'_comp_whiskerLeft_mapComp'_assoc _ _ _ _ _ f h₀₂ h₁₃ (by cat_disch)]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.ConnectedComponents

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.IsChain Zag (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
f : (x : J) → Zigzag x j₂ → (ConnectedComponents.mk j₂).Component := ⋯
i : J
hi : i ∈ l
⊢ Zigzag j₂ j₂

Tactic:
apply Relation.ReflTransGen.refl

Goal state after: