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

Goal state before:
pp: case neg
ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left✝ : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
hKP : P (Set.univ \ KP) < ENNReal.ofReal ε
⊢ |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| ≤ 6 * √ε

Tactic:
obtain ⟨KP', _, hKP'co, hKP'cl, hKP'⟩ := MeasurableSet.exists_isCompact_isClosed_sdiff_lt
    (MeasurableSet.univ) (measure_ne_top P' Set.univ) (ofReal_pos.mpr hε).ne'

Goal state after:
case neg
ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left✝¹ : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
hKP : P (Set.univ \ KP) < ENNReal.ofReal ε
KP' : Set E
left✝ : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
hKP' : P' (Set.univ \ KP') < ENNReal.ofReal ε
⊢ |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| ≤ 6 * √ε
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
ε : ℝ
hε : 0 < ε
x : ↑(sphere 0 1)
this✝ : Nontrivial E
this : ∀ {ε : ℝ}, 0 < ε → ε ≤ 2 → ↑(toSphereBallBound (dim E) ε) * μ (ball 0 1) ≤ μ.toSphere (ball x ε)
hε₂ : ¬ε ≤ 2
⊢ ↑(toSphereBallBound (dim E) ε) * μ (ball 0 1) ≤ μ.toSphere (ball x ε)

pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ↑(toSphereBallBound (dim E) ε) * μ (ball 0 1) ≤ μ.toSphere (ball x ε)

Tactic:
· trans μ.toSphere (ball x (min ε 2))
    · simpa [Real.toNNReal_monotone.map_min, toSphereBallBound]
        using this (ε := min ε 2) (by simp [hε]) (by simp)
    · gcongr
      simp

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
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ↑(toSphereBallBound (dim E) ε) * μ (ball 0 1) ≤ μ.toSphere (ball x ε)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ -2 / (l - ↑x) ^ 3 = deriv (fun x2 ↦ 1 / (x2 - ↑x) ^ 2 - 1 / ↑x ^ 2) l

Tactic:
deriv_fun_sub (.fun_div (by fun_prop) (by fun_prop) (by simpa)) (by fun_prop),

Goal state after:
case neg
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ -2 / (l - ↑x) ^ 3 = deriv (fun x2 ↦ 1 / (x2 - ↑x) ^ 2) l - deriv (fun x2 ↦ 1 / ↑x ^ 2) l
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: case refine_2
x : ℝ
hx : x ∈ Ioo 0 1
⊢ x ∈ range sigmoid

Tactic:
· replace hx : 0 < x⁻¹ - 1 := by rwa [sub_pos, one_lt_inv_iff₀]
    exact ⟨-(log (x⁻¹ - 1)), by simp [sigmoid_def, exp_log hx]⟩

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

Goal state before:
pp: case inr
n i : ℕ
hi : i ≤ n
hn : n ≠ 0
h₁ : 0 < (-1) ^ i * ∏ x ∈ Finset.range i, (node n i - node n x)
h₂ : 0 < ∏ j ∈ Finset.Ioc i n, (node n i - node n j)
union : (Finset.range (n + 1)).erase i = Finset.range i ∪ Finset.Ioc i n
disjoint : Disjoint (Finset.range i) (Finset.Ioc i n)
⊢ 0 < (-1) ^ i * ∏ j ∈ Finset.range i ∪ Finset.Ioc i n, (node n i - node n j)

Tactic:
Finset.prod_union disjoint,

Goal state after:
case inr
n i : ℕ
hi : i ≤ n
hn : n ≠ 0
h₁ : 0 < (-1) ^ i * ∏ x ∈ Finset.range i, (node n i - node n x)
h₂ : 0 < ∏ j ∈ Finset.Ioc i n, (node n i - node n j)
union : (Finset.range (n + 1)).erase i = Finset.range i ∪ Finset.Ioc i n
disjoint : Disjoint (Finset.range i) (Finset.Ioc i n)
⊢ 0 < (-1) ^ i * ((∏ x ∈ Finset.range i, (node n i - node n x)) * ∏ x ∈ Finset.Ioc i n, (node n i - node n x))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: case e'_3
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
⊢ (-1) ^ k - 1 = Complex.exp (↑π * I) ^ k - 1

Tactic:
Complex.exp_pi_mul_I

Goal state after:
case e'_3
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
⊢ (-1) ^ k - 1 = (-1) ^ k - 1
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case hasSum
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
z : ℂ
⊢ z ∈ Metric.eball 0 ↑r → HasSum (fun n ↦ (L.weierstrassPExceptSeries l₀ x n) fun x ↦ z) (℘[L - l₀] (x + z))

Tactic:
hz

Goal state after:
case hasSum
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
z : ℂ
hz : z ∈ Metric.eball 0 ↑r
⊢ HasSum (fun n ↦ (L.weierstrassPExceptSeries l₀ x n) fun x ↦ z) (℘[L - l₀] (x + z))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: m n : ℤ
⊢ ↑|m| ≤ ‖![n, m]‖

Tactic:
by
  simp only [EisensteinSeries.norm_eq_max_natAbs, Fin.isValue, Matrix.cons_val_zero,
    Matrix.cons_val_one, Matrix.cons_val_fin_one, Nat.cast_max, le_sup_iff]
  right
  rw [Int.abs_eq_natAbs]
  exact le_refl _

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

Goal state before:
pp: L : PeriodPair
z : ℂ
⊢ z ∈ (↑L.lattice \ {0})ᶜ →
    (L.relation * id ^ 6) z =
      (℘'[L - 0] z * z ^ 3 - 2) ^ 2 - 4 * (℘[L - 0] z * z ^ 2 + 1) ^ 3 + L.g₂ * (℘[L - 0] z * z ^ 6 + z ^ 4) +
        L.g₃ * z ^ 6

Tactic:
hz

Goal state after:
L : PeriodPair
z : ℂ
hz : z ∈ (↑L.lattice \ {0})ᶜ
⊢ (L.relation * id ^ 6) z =
    (℘'[L - 0] z * z ^ 3 - 2) ^ 2 - 4 * (℘[L - 0] z * z ^ 2 + 1) ^ 3 + L.g₂ * (℘[L - 0] z * z ^ 6 + z ^ 4) +
      L.g₃ * z ^ 6
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
K : Set β
hK : K ⊆ s
⊢ IsCompact K → TendstoUniformlyOn (fun x1 x2 ↦ ∑ i ∈ x1, f i x2) (fun x ↦ ∑' (n : α), f n x) atTop K

Tactic:
hKc

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
K : Set β
hK : K ⊆ s
hKc : IsCompact K
⊢ TendstoUniformlyOn (fun x1 x2 ↦ ∑ i ∈ x1, f i x2) (fun x ↦ ∑' (n : α), f n x) atTop K
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 : α), ∀ k ∈ K, ‖f n k‖ ≤ u n
K : Set β
hK : K ⊆ s
⊢ IsCompact K → ∃ u, Summable u ∧ ∀ᶠ (n : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n

Tactic:
hKc

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 : α), ∀ k ∈ K, ‖f n k‖ ≤ u n
K : Set β
hK : K ⊆ s
hKc : IsCompact K
⊢ ∃ u, Summable u ∧ ∀ᶠ (n : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℂ
hz : z ≠ 0
d k : ℤ
hk : 2 ≤ k
⊢ Summable fun c ↦ ((↑c * z + ↑d) ^ k)⁻¹

Tactic:
apply summable_inv_of_isBigO_rpow_inv (a := k) (by norm_cast)
  lift k to ℕ using (by lia)
  simp only [zpow_natCast, Int.cast_natCast, Real.rpow_natCast, ← inv_pow, ← abs_inv]
  apply (linear_inv_isBigO_left d hz).abs_right.pow

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

Goal state before:
pp: L : PeriodPair
⊢ 7 ≤ ENat.map Nat.cast (analyticOrderAt (L.relation * id ^ 6) 0)

Tactic:
refine ENat.monotone_map_iff.mpr Nat.mono_cast
    ((natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero (by fun_prop)).mpr fun i hi₁ ↦ ?_)

Goal state after:
L : PeriodPair
i : ℕ
hi₁ : i < 7
⊢ iteratedDeriv i (L.relation * id ^ 6) 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ (↑n + 1) ^ 2 ≠ 0

Tactic:
simp [Nat.cast_add_one_ne_zero n]

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

Goal state before:
pp: case refine_1
Z : Set ℂ
hZC : IsCompact Z
u : ℕ → ℝ
hu : Summable u
hu2 : ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j
n : ℕ
z : ℂ
⊢ z ∈ Z → ‖sineTerm z n‖ ≤ u n

Tactic:
hz

Goal state after:
case refine_1
Z : Set ℂ
hZC : IsCompact Z
u : ℕ → ℝ
hu : Summable u
hu2 : ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j
n : ℕ
z : ℂ
hz : z ∈ Z
⊢ ‖sineTerm z n‖ ≤ u n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k d : ℕ
z : ℂ
⊢ z ∈ ℂ_ℤ →
    iteratedDeriv k (fun z ↦ cotTerm z d) z =
      (fun z ↦ (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))) z

Tactic:
hz

Goal state after:
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ iteratedDeriv k (fun z ↦ cotTerm z d) z =
    (fun z ↦ (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))) z
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
p : ℕ
hp : 2 ≤ p
hpn : p ∣ n
⊢ 3 ≤ p

Tactic:
rcases hp.eq_or_lt with rfl | h

Goal state after:
case inl
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
hp : 2 ≤ 2
hpn : 2 ∣ n
⊢ 3 ≤ 2

case inr
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
p : ℕ
hp : 2 ≤ p
hpn : p ∣ n
h : 2 < p
⊢ 3 ≤ p
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k d : ℕ
z : ℂ
⊢ z ∈ ℍₒ →
    iteratedDerivWithin k (fun z ↦ cotTerm z d) (range Int.cast)ᶜ z =
      (fun z ↦ (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))) z

Tactic:
hz

Goal state after:
k d : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ iteratedDerivWithin k (fun z ↦ cotTerm z d) (range Int.cast)ᶜ z =
    (fun z ↦ (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))) z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
K : Set ℂ
hK : K ⊆ ℍₒ
⊢ IsCompact K → ∃ u, Summable u ∧ ∀ (n : ℕ), ∀ k_1 ∈ K, ‖iteratedDerivWithin k (fun z ↦ cotTerm z n) ℍₒ k_1‖ ≤ u n

Tactic:
hKc

Goal state after:
k : ℕ
hk : 1 ≤ k
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
⊢ ∃ u, Summable u ∧ ∀ (n : ℕ), ∀ k_1 ∈ K, ‖iteratedDerivWithin k (fun z ↦ cotTerm z n) ℍₒ k_1‖ ≤ u n
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: n : ℕ
⊢ √5 * (√5)⁻¹ * (1 / 2 + √5 * (-1 / 2)) ^ n = (1 / 2 + √5 * (-1 / 2)) ^ n

Tactic:
have nz : √5 ≠ 0 := by norm_num

Goal state after:
n : ℕ
nz : √5 ≠ 0
⊢ √5 * (√5)⁻¹ * (1 / 2 + √5 * (-1 / 2)) ^ n = (1 / 2 + √5 * (-1 / 2)) ^ n
Module: Mathlib.CategoryTheory.Abelian.Projective.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
hP : Projective P
⊢ (preadditiveCoyonedaObj P).PreservesHomology

Tactic:
have := (projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj P).mp hP
  apply Functor.preservesHomology_of_preservesEpis_and_kernels

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
⊢ x₀ = x₀ + ↑0

Tactic:
simp [-Nat.cast_add]

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

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

Tactic:
exact hf.neg.integral_le_sum

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 n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, ↑(c n) * l - u (c n) ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ ↑(c b) * l - u (c b) ≤ ε * ↑(c b)
M : ℕ := (image (fun i ↦ c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
aN' : a ≤ N - 1
cNn : c (N - 1) ≤ n
⊢ ↑n * l - u n ≤ ↑(c N) * l - u (c (N - 1))

Tactic:
gcongr
        exact hmono cNn

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
⊢ ∃ ε, d + ε * (1 + l) < l ∧ 0 < ε

Tactic:
have L : Tendsto (fun ε => d + ε * (1 + l)) (𝓝[>] 0) (𝓝 (d + 0 * (1 + l))) := by
        apply Tendsto.mono_left _ nhdsWithin_le_nhds
        exact tendsto_const_nhds.add (tendsto_id.mul tendsto_const_nhds)
      simp only [zero_mul, add_zero] at L
      exact (((tendsto_order.1 L).2 l hd).and self_mem_nhdsWithin).exists

Goal state after:
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
⊢ IntegrableOn f (Ioi ↑N) volume

Tactic:
by
  refine integrableOn_Ioi_of_intervalIntegral_norm_bounded (∑' (n : ℕ), f (n + N : ℕ)) _ ?_
    (tendsto_atTop_add_const_right atTop (N : ℝ) tendsto_natCast_atTop_atTop) ?_
  · intro n
    rw [← intervalIntegrable_iff_integrableOn_Ioc_of_le (by grind)]
    exact (anti.mono <| by grind [uIcc_of_le]).intervalIntegrable
  · filter_upwards [eventually_gt_atTop 0] with M hM
    calc
      _ = ∫ x in N..M+N, f x := by
        refine intervalIntegral.integral_congr_uIoo fun x ↦ ?_
        grind [Real.norm_of_nonneg, uIoo_of_le]
      _ ≤ ∑ n ∈ Finset.range M, f (n + N : ℕ) := by
        convert! AntitoneOn.integral_le_sum (anti.mono _) using 2 <;> grind
      _ ≤ _ := by grind [summable.sum_le_tsum, Nat.cast_pos]

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

Goal state before:
pp: case inl
c : ℝ
hc : 1 < c
cpos : 0 < c
⊢ (1 - c⁻¹) * c ^ 0 ≤ ↑⌊c ^ 0⌋₊

pp: case inr
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i ≠ 0
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊

Tactic:
· simp only [pow_zero, Nat.floor_one, Nat.cast_one, mul_one, sub_le_self_iff, inv_nonneg, cpos.le]

Goal state after:
case inr
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i ≠ 0
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊
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
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'
F : A ⥤ A'
G : B ⥤ B'
H : T ⥤ T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst✝⁴ : IsFiltered B
inst✝³ : R.Final
inst✝² : R'.Final
inst✝¹ : F.Final
inst✝ : G.Final
x✝ : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this✝¹ : (R ⋙ H).Final
this✝ :
  StructuredArrow.map₂ u₂ iR.hom ≅
    StructuredArrow.post j₂ G R' ⋙ StructuredArrow.map₂ u₂ iR.hom ⋙ StructuredArrow.pre (L'.obj i₂) R H
this : (StructuredArrow.map₂ u₂ iR.hom).Final
⊢ IsConnected
    (Comma (StructuredArrow.map₂ (𝟙 (L'.obj { left := i₂, right := j₂, hom := u₂ }.left)) iL.hom)
      (StructuredArrow.map₂ { left := i₂, right := j₂, hom := u₂ }.hom (inv iR.inv)))

Tactic:
IsIso.Iso.inv_inv

Goal state after:
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
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'
F : A ⥤ A'
G : B ⥤ B'
H : T ⥤ T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst✝⁴ : IsFiltered B
inst✝³ : R.Final
inst✝² : R'.Final
inst✝¹ : F.Final
inst✝ : G.Final
x✝ : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this✝¹ : (R ⋙ H).Final
this✝ :
  StructuredArrow.map₂ u₂ iR.hom ≅
    StructuredArrow.post j₂ G R' ⋙ StructuredArrow.map₂ u₂ iR.hom ⋙ StructuredArrow.pre (L'.obj i₂) R H
this : (StructuredArrow.map₂ u₂ iR.hom).Final
⊢ IsConnected
    (Comma (StructuredArrow.map₂ (𝟙 (L'.obj { left := i₂, right := j₂, hom := u₂ }.left)) iL.hom)
      (StructuredArrow.map₂ { left := i₂, right := j₂, hom := u₂ }.hom iR.hom))
Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ Cᵒᵖ ⥤ Type v
hF : ∀ (i : I), IsIndObject (F.obj i)
⊢ IsIndObject (colimit F)

Tactic:
have : IsFiltered (CostructuredArrow yoneda (colimit F)) :=
    IndizationClosedUnderFilteredColimitsAux.isFiltered F hF
  refine (isIndObject_iff _).mpr ⟨this, ?_⟩
  -- It remains to show that `CostructuredArrow yoneda (colimit F)` is finally small. Because we
  -- have already shown it is filtered, it suffices to exhibit a small weakly terminal set. For this
  -- we use that all the `CostructuredArrow yoneda (F.obj i)` have small weakly terminal sets.
  have : ∀ i, ∃ (s : Set (CostructuredArrow yoneda (F.obj i))) (_ : Small.{v} s),
      ∀ i, ∃ j ∈ s, Nonempty (i ⟶ j) :=
    fun i => (hF i).finallySmall.exists_small_weakly_terminal_set
  choose s hs j hjs hj using this
  refine finallySmall_of_small_weakly_terminal_set
    (⋃ i, (map (colimit.ι F i)).obj '' (s i)) (fun A => ?_)
  obtain ⟨i, y, hy⟩ := FunctorToTypes.jointly_surjective'.{v, v} F _ (yonedaEquiv A.hom)
  let y' : CostructuredArrow yoneda (F.obj i) := mk (yonedaEquiv.symm y)
  obtain ⟨x⟩ := hj _ y'
  refine ⟨(map (colimit.ι F i)).obj (j i y'), ?_, ⟨?_⟩⟩
  · simp only [Set.mem_iUnion, Set.mem_image]
    exact ⟨i, j i y', hjs _ _, rfl⟩
  · refine ?_ ≫ (map (colimit.ι F i)).map x
    refine homMk (𝟙 A.left) (yonedaEquiv.injective ?_)
    simp [-EmbeddingLike.apply_eq_iff_eq, hy, yonedaEquiv_comp, y']

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset

Goal state before:
pp: case h₀
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteCoproducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasCoproduct f
S : Finset (Discrete α)
v : ↥S
⊢ ∀ b ∈ S.attach, b ≠ v → Sigma.ι (fun x ↦ f (↑x).as) v ≫ Sigma.π (fun a ↦ f (↑a).as) b ≫ Sigma.ι f (↑b).as = 0

Tactic:
intro b hb hb₁
    rw [Sigma.ι_π_of_ne_assoc _ (Ne.symm hb₁), zero_comp]

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

Goal state before:
pp: α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
⊢ IsIso (colimitPointwiseProductToProductColimit F)

Tactic:
by
  -- We follow the proof in [Kashiwara2006], Prop. 3.1.11(ii)
  refine (isIso_iff_bijective _).2 ⟨fun y y' hy => ?_, fun x => ?_⟩
  · obtain ⟨ky, yk₀, hyk₀⟩ := Types.jointly_surjective' y
    obtain ⟨ky', yk₀', hyk₀'⟩ := Types.jointly_surjective' y'
    let k := IsFiltered.max ky ky'
    let yk : (pointwiseProduct F).obj k :=
      (pointwiseProduct F).map (IsFiltered.leftToMax ky ky') yk₀
    let yk' : (pointwiseProduct F).obj k :=
      (pointwiseProduct F).map (IsFiltered.rightToMax ky ky') yk₀'
    obtain rfl : y = colimit.ι (pointwiseProduct F) k yk := by
      simp only [k, yk, colimit.w_apply, hyk₀]
    obtain rfl : y' = colimit.ι (pointwiseProduct F) k yk' := by
      simp only [k, yk', colimit.w_apply, hyk₀']
    dsimp at yk yk'
    have hch : ∀ (s : α), ∃ (i' : I s) (hi' : k s ⟶ i'),
        (F s).map hi' (Pi.π (fun s => (F s).obj (k s)) s yk) =
          (F s).map hi' (Pi.π (fun s => (F s).obj (k s)) s yk') := by
      intro s
      have hy₁ := congr_hom (ι_colimitPointwiseProductToProductColimit_π F k s) yk
      have hy₂ := congr_hom (ι_colimitPointwiseProductToProductColimit_π F k s) yk'
      dsimp at hy₁ hy₂ hy
      rw [← hy, hy₁, Types.FilteredColimit.colimit_eq_iff] at hy₂
      obtain ⟨i₀, f₀, g₀, h₀⟩ := hy₂
      refine ⟨IsFiltered.coeq f₀ g₀, f₀ ≫ IsFiltered.coeqHom f₀ g₀, ?_⟩
      conv_rhs => rw [IsFiltered.coeq_condition]
      dsimp [Functor.pi] at h₀
      simp [h₀]
    choose k' f hk' using hch
    apply Types.colimit_sound' f f
    exact Types.limit_ext' _ _ _ (fun ⟨s⟩ => by simpa [Functor.pi, Pi.map_π_apply] using hk' s)
  · have hch : ∀ (s : α), ∃ (i : I s) (xi : (F s).obj i), colimit.ι (F s) i xi =
        Pi.π (fun s => colimit (F s)) s x := fun s => Types.jointly_surjective' _
    choose k p hk using hch
    refine ⟨colimit.ι (pointwiseProduct F) k ((Types.productIso _).inv p), ?_⟩
    refine Types.limit_ext' _ _ _ (fun ⟨s⟩ => ?_)
    have := congr_hom (ι_colimitPointwiseProductToProductColimit_π F k s)
      ((Types.productIso _).inv p)
    exact this.trans (by simpa [Functor.pi] using hk _)

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
⊢ ⟦Over.mk (p.hom ≫ f)⟧ = ⟦Over.mk (𝟙 Q)⟧

Tactic:
← hp

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
p : Over P
hpbar : pseudoApply f ⟦p⟧ = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
hp : ⟦p⟧ = pbar
⊢ ⟦Over.mk (p.hom ≫ f)⟧ = ⟦Over.mk (𝟙 Q)⟧
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
a' : ↑y.left
ha' : (ModuleCat.Hom.hom y.hom) a' = a
⊢ a ∈ (ModuleCat.Hom.hom x.hom).range

Tactic:
obtain ⟨a'', ha''⟩ := (ModuleCat.epi_iff_surjective q).1 hq a'

Goal state after:
case refine_2
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
a' : ↑y.left
ha' : (ModuleCat.Hom.hom y.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom q) a'' = a'
⊢ a ∈ (ModuleCat.Hom.hom x.hom).range