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

Goal state before:
pp: case refine_2
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
⊢ (∑ x ∈ s, if ↑x = l₀ then 0 else -2 / (l - ↑x) ^ 3) =
    deriv (fun x2 ↦ ∑ x ∈ s, if ↑x = l₀ then 0 else 1 / (x2 - ↑x) ^ 2 - 1 / ↑x ^ 2) l

Tactic:
deriv_fun_sum

Goal state after:
case refine_2
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
⊢ (∑ x ∈ s, if ↑x = l₀ then 0 else -2 / (l - ↑x) ^ 3) =
    ∑ i ∈ s, deriv (fun x2 ↦ if ↑i = l₀ then 0 else 1 / (x2 - ↑i) ^ 2 - 1 / ↑i ^ 2) l

case refine_2
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
⊢ ∀ i ∈ s, DifferentiableAt ℂ (fun x2 ↦ if ↑i = l₀ then 0 else 1 / (x2 - ↑i) ^ 2 - 1 / ↑i ^ 2) l
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b c : ℂ
⊢ (fun z ↦ (a.regularizedGaussHGFunSeries b c).sum z) = fun z ↦ (b.regularizedGaussHGFunSeries a c).sum z

Tactic:
regularizedGaussHGFunSeries_symm

Goal state after:
a b c : ℂ
⊢ (fun z ↦ (b.regularizedGaussHGFunSeries a c).sum z) = fun z ↦ (b.regularizedGaussHGFunSeries a c).sum z
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: x : ℝ
⊢ (1 + rexp (-x))⁻¹ * rexp (-x) = 1 - (1 + rexp (-x))⁻¹

Tactic:
field

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

Goal state before:
pp: case inr.inr
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
⊢ HasStrictDerivAt arcsin (1 / √(1 - x ^ 2)) x ∧ ContDiffAt ℝ ω arcsin x

Tactic:
· have : 1 - x ^ 2 < 0 := by nlinarith [h₂]
    rw [sqrt_eq_zero'.2 this.le, div_zero]
    have : arcsin =ᶠ[𝓝 x] fun _ => π / 2 := (lt_mem_nhds h₂).mono fun y hy => arcsin_of_one_le hy.le
    exact ⟨(hasStrictDerivAt_const x _).congr_of_eventuallyEq this.symm,
      contDiffAt_const.congr_of_eventuallyEq this⟩

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
k : ℕ
⊢ 1 / (2 * ↑k + 1) * (1 / (2 * (↑m + 1) + 1)) ^ (2 * k) =
    (↑m + 1 + 1 / 2) * (2 * (1 / (2 * ↑k + 1)) * ((1 / (2 * (↑m + 1) + 1)) ^ (2 * k) * (1 / (2 * (↑m + 1) + 1)) ^ 1))

Tactic:
field

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

Goal state before:
pp: m : ℕ
f : ℕ → ℝ := fun k ↦ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
x : ℝ
hx : x ≠ 0
⊢ 1 + x⁻¹ = (x + 1) / x

Tactic:
field

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

Goal state before:
pp: ⊢ IntervalIntegrable (fun x ↦ √(1 - x ^ 2)⁻¹) volume (-1) 1

Tactic:
rw [intervalIntegrable_iff]
  refine integrableOn_deriv_of_nonneg continuous_arccos.neg.continuousOn (fun x hx ↦ ?_) (by simp)
  simpa using! (hasDerivAt_arccos (by aesop) (by aesop)).neg

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

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

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

Goal state after:
n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ∫ (θ : ℝ) in 0..↑n * π, deriv sin θ = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n i : ℕ
hi : i ∈ Finset.Iic n
hn : n ≠ 0
⊢ ↑n * (↑i * π / ↑n) = ↑i * π

Tactic:
field

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

Goal state before:
pp: case a
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
this :
  (∑ i ∈ range n, Complex.exp (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π) * I)) * (Complex.exp (↑k / (2 * ↑n) * ↑π * I))⁻¹ *
      (Complex.exp (↑k / ↑n * ↑π * I) - 1) =
    (-1) ^ k - 1
s a b t : ℂ
h : s * a⁻¹ * b = t
ha : a ≠ 0
hb : b ≠ 0
⊢ s + t * a / b - (a / b * t + s * a⁻¹ * b * a / b) = 0

Tactic:
field

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ 2 * ↑q.den * (↑q.num / ↑q.den * ↑π * I) = ↑q.num * (2 * ↑π * I)

Tactic:
field

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ π / ↑n * ↑n = π

Tactic:
field

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
⊢ ∃ k, 2 * cos (↑r * π) = ↑k

Tactic:
rw [← (Real.isIntegral_two_mul_cos_rat_mul_pi r).exists_int_iff_exists_rat]
    exact ⟨2 * hcos.choose, by push_cast; linarith [hcos.choose_spec]⟩

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

Goal state before:
pp: L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp :
  ¬↑((Equiv.prodCongrLeft fun x ↦
              { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
            (Prod.map some id p)).2 =
      l₀
hpx : ‖↑p.2 - x‖ ≠ 0
hxz : z ≠ x
⊢ ‖↑p.1 + 2‖ * ((‖↑p.2 - x‖ ^ 3)⁻¹ / ‖↑p.2 - x‖ ^ p.1) * ‖z - x‖ ^ (p.1 + 1) =
    ‖↑p.1 + 2‖ * (‖z - x‖ ^ p.1 / ‖↑p.2 - x‖ ^ p.1) * ((‖↑p.2 - x‖ ^ 3)⁻¹ * ‖z - x‖)

Tactic:
field

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

Goal state before:
pp: case neg
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
i : ℕ
hrange : i ∈ range (2 * n)
h✝ : ¬i = 0
⊢ ∫ (a : ℝ), eval a (T ℝ ↑i) ∂measureT = sumZeroes n (T ℝ ↑i)

Tactic:
case neg hi =>
      have : ¬ (2 * n : ℤ) ∣ i := by
        refine (Int.not_dvd_iff_lt_mul_succ _ (by grind)).mpr ⟨0, ⟨by grind, ?_⟩⟩
        rw_mod_cast [zero_add, mul_one]
        exact mem_range.mp hrange
      rw [integral_eval_T_real_measureT_of_ne_zero (by grind), sumZeroes_T_of_not_dvd this]

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

Goal state before:
pp: case succ
L : PeriodPair
l : ℂ
n✝ : ℕ
⊢ (↑n✝ + 1 + 1) * L.sumInvPow l (n✝ + 1 + 2) =
    (↑n✝ + 1 + 1) * ((↑n✝ + 1) * ↑n✝!) * L.sumInvPow l (n✝ + 1 + 2) / ((↑n✝ + 1) * ↑n✝!)

Tactic:
field

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

Goal state before:
pp: z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
⊢ r z * ‖x‖ ≤ ‖↑(x 0) * ↑z + ↑(x 1)‖

Tactic:
rw [norm_eq_max_natAbs, h11, norm_mul, norm_real, norm_norm, norm_eq_max_natAbs]

Goal state after:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
⊢ r z * ↑(max (x 0).natAbs (x 1).natAbs) ≤
    ‖↑(x 0) / ↑↑(max (x 0).natAbs (x 1).natAbs) * ↑z + ↑(x 1) / ↑↑(max (x 0).natAbs (x 1).natAbs)‖ *
      ↑(max (x 0).natAbs (x 1).natAbs)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l : ℂ
n : ℕ
⊢ iteratedDeriv n ℘'[L - l] l = ↑(n + 2)! * L.sumInvPow l (n + 3)

Tactic:
by
  have : iteratedDeriv n ℘'[L - l] l / n ! = (↑n + 1) * (↑n + 2) * L.sumInvPow l (n + 3) := by
    simpa using congr($((L.analyticAt_derivWeierstrassPExcept l).hasFPowerSeriesAt
      |>.eq_formalMultilinearSeries (L.hasFPowerSeriesAt_derivWeierstrassPExcept l)).coeff n)
  simp [div_eq_iff, Nat.factorial_ne_zero, Nat.factorial_succ] at this ⊢
  grind

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

Goal state before:
pp: case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : ↑↑k * π = ↑n * arccos x
hk' : ↑↑k = ↑n * (arccos x / π)
⊢ ∃ k ≤ n, x = cos (↑k * π / ↑n)

Tactic:
simp only [Int.cast_natCast] at hk hk'

Goal state after:
case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : ↑k * π = ↑n * arccos x
hk' : ↑k = ↑n * (arccos x / π)
⊢ ∃ k ≤ n, x = cos (↑k * π / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z x : ℂ
hx : ∀ (l : ↥L.lattice), ‖z - x‖ < ‖↑l - x‖
⊢ Summable (Function.uncurry fun b c ↦ L.weierstrassPSummand x b c * (z - x) ^ b)

Tactic:
by
  simp_rw [← L.weierstrassPExceptSummand_of_notMem _ L.ω₁_div_two_notMem_lattice]
  refine L.summable_weierstrassPExceptSummand _ z x fun l hl ↦ hx l

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

Goal state before:
pp: case neg
L : PeriodPair
z : ℂ
hz0 : ¬z = 0
hz : z ∉ L.lattice
⊢ (℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃) * z ^ 6 =
    ((℘'[L] z + 2 / z ^ 3) * z ^ 3 - 2) ^ 2 - 4 * ((℘[L] z + -(z ^ 2)⁻¹) * z ^ 2 + 1) ^ 3 +
        L.g₂ * ((℘[L] z + -(z ^ 2)⁻¹) * z ^ 6 + z ^ 4) +
      L.g₃ * z ^ 6

Tactic:
field

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

Goal state before:
pp: z : ℂ
h1 : cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
h2 : cexp (-z * I) - cexp (z * I) = cexp (-(z * I)) * (1 - cexp (2 * I * z))
⊢ cexp (-(z * I)) * (cexp (2 * I * z) + 1) / 2 / (cexp (-(z * I)) * (1 - cexp (2 * I * z)) * I / 2) =
    (cexp (2 * I * z) + 1) / (I * (1 - cexp (2 * I * z)))

Tactic:
field

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

Goal state before:
pp: R : Type u_1
a b u₀ : R
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ha_pos : 0 < a
ha_ne : a ≠ 1
h0 : b / (1 - a) < u₀
n : ℕ
⊢ b / (1 - a) < arithGeom a b u₀ n

Tactic:
induction n with
  | zero => exact h0
  | succ n hn =>
    calc b / (1 - a)
    _ = a * (b / (1 - a)) + b := by grind
    _ < a * arithGeom a b u₀ n + b := by gcongr

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

Goal state before:
pp: n : ℕ
hn0 : n = 0
⊢ fib (-↑n + 1) = (-1) ^ (n + 1) * ↑(Nat.fib n) + (-1) ^ (1 + (n + 1)) * ↑(Nat.fib (n + 1))

Tactic:
then

Goal state after:
n : ℕ
hn0 : n = 0
⊢ fib (-↑n + 1) = (-1) ^ (n + 1) * ↑(Nat.fib n) + (-1) ^ (1 + (n + 1)) * ↑(Nat.fib (n + 1))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
i : ℕ
h2 : ¬x - (↑i + 1) = 0
h3 : ¬(↑i + 1) ^ 2 + -x ^ 2 = 0
h1 : ¬x + (↑i + 1) = 0
⊢ -(2 * x ^ (2 - 1) * 1) / (↑i + 1) ^ 2 / (1 + -x ^ 2 / (↑i + 1) ^ 2) = 1 / (x - (↑i + 1)) + 1 / (x + (↑i + 1))

Tactic:
field

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

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

Tactic:
field

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

Goal state before:
pp: h₁ : ∀ (n : ℕ), ↑(fib (n + 1)) / ↑(fib n) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
⊢ |ψ / φ| < 1

Tactic:
abs_div,

Goal state after:
h₁ : ∀ (n : ℕ), ↑(fib (n + 1)) / ↑(fib n) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
⊢ |ψ| / |φ| < 1
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ -ψ < 1

Tactic:
← inv_goldenRatio

Goal state after:
⊢ φ⁻¹ < 1
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: i : ℕ
hi : i ∈ Finset.range fibRec.order
⊢ (fun n ↦ ↑(Nat.fib n)) i = (fun n ↦ (φ ^ n - ψ ^ n) / √5) i

Tactic:
fin_cases hi <;> simp

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

Goal state before:
pp: case hf
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (↑k) (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z

Tactic:
exact ContDiffWithinAt.mul (by fun_prop) (cot_pi_mul_contDiffWithinAt k
      (UpperHalfPlane.coe_mem_integerComplement ⟨z, hz⟩))

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
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / ↑(c x) - l‖ ≤ c_1 * ‖1‖
n : ℕ
hn : ‖u (c n) / ↑(c n) - l‖ ≤ ε * ‖1‖
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
cnpos : 0 < c n
⊢ u (c n) - ↑(c n) * l = (u (c n) / ↑(c n) - l) * ↑(c n)

Tactic:
field

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
ε : ℝ
ε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, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ u (c b) - ↑(c b) * l ≤ ε * ↑(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
cNn : c (N - 1) ≤ n
A : a ≤ N - 1
B : N - 1 + 1 = N
this : ↑(c (N - 1 + 1)) ≤ (1 + ε) * ↑(c (N - 1))
⊢ ↑(c N) ≤ (1 + ε) * ↑(c (N - 1))

Tactic:
B

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 : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ u (c b) - ↑(c b) * l ≤ ε * ↑(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
cNn : c (N - 1) ≤ n
A : a ≤ N - 1
B : N - 1 + 1 = N
this : ↑(c N) ≤ (1 + ε) * ↑(c (N - 1))
⊢ ↑(c N) ≤ (1 + ε) * ↑(c (N - 1))
Module: Mathlib.CategoryTheory.Generator.Preadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : ObjectProperty C
h𝒢 : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = 0) → f = 0
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ ∀ (G : C), P G → ∀ (h : Y ⟶ G), (f - g) ≫ h = 0

Tactic:
simpa only [Preadditive.sub_comp, sub_eq_zero] using hfg

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
hG : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = 0) → f = 0
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ ∀ (h : Y ⟶ G), (f - g) ≫ h = 0

Tactic:
simpa only [Preadditive.sub_comp, sub_eq_zero] using hfg

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 : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / ↑(c x) - l‖ ≤ c_1 * ‖1‖
n : ℕ
hn : ‖u (c n) / ↑(c n) - l‖ ≤ ε * ‖1‖
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
cnpos : 0 < c n
⊢ ↑(c n) * l - u (c n) = -(u (c n) / ↑(c n) - l) * ↑(c n)

Tactic:
field

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case c0
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : ↑a ≤ ↑i ∧ ↑i + 1 ≤ ↑b
⊢ 0 ≤ g ↑i

Tactic:
gpos

Goal state after:
case c0
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : ↑a ≤ ↑i ∧ ↑i + 1 ≤ ↑b
⊢ g (↑b - 1) ≤ g ↑i
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case c0
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : ↑a ≤ ↑i ∧ ↑i + 1 ≤ ↑b
⊢ 0 ≤ g (x - 1)

Tactic:
gpos

Goal state after:
case c0
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : ↑a ≤ ↑i ∧ ↑i + 1 ≤ ↑b
⊢ g (↑a - 1) ≤ g (x - 1)
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ε : l + ε * (1 + ε + l) < d
εpos : 0 < ε
n : ℕ
hn : u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
npos : 0 < n
⊢ (↑n * l + ε * (1 + ε + l) * ↑n) / ↑n = l + ε * (1 + ε + l)

Tactic:
field

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

Goal state before:
pp: N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
this : c ^ 3 = c ^ 2 * c
⊢ c ^ 2 * (c - 1) ≤ c ^ 3 * (1 - c⁻¹ ^ 2)

Tactic:
simp only [mul_sub, this, mul_one, inv_pow, sub_le_sub_iff_left]

Goal state after:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
this : c ^ 3 = c ^ 2 * c
⊢ c ^ 2 * c * (c ^ 2)⁻¹ ≤ c ^ 2
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case e_a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹) = c ^ 5 * (c - 1)⁻¹ ^ 3

Tactic:
field

Goal state after:
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
this : ∀ (d : T), IsCofiltered (CostructuredArrow L d)
⊢ (fst L R).Initial

Tactic:
exact initial_fst_of_isCofiltered_costructuredArrow L R

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
B : C
hB : Injective B
⊢ Injective ((preadditiveCoyonedaObj G).obj B)

Tactic:
← Module.injective_iff_injective_object

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
B : C
hB : Injective B
⊢ Module.Injective (End G)ᵐᵒᵖ ↑((preadditiveCoyonedaObj G).1 B)
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
y : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex ↑n
this : HasDerivedCategory C
x : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex ↑n
⊢ R.extEquivCohomologyClass.symm (CohomologyClass.mk x + y) =
    R.extEquivCohomologyClass.symm (CohomologyClass.mk x) + R.extEquivCohomologyClass.symm y

Tactic:
obtain ⟨y, rfl⟩ := y.mk_surjective

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
this : HasDerivedCategory C
x y : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex ↑n
⊢ R.extEquivCohomologyClass.symm (CohomologyClass.mk x + CohomologyClass.mk y) =
    R.extEquivCohomologyClass.symm (CohomologyClass.mk x) + R.extEquivCohomologyClass.symm (CohomologyClass.mk y)
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
x y : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex ↑n
⊢ R.extEquivCohomologyClass.symm (x + y) = R.extEquivCohomologyClass.symm x + R.extEquivCohomologyClass.symm y

Tactic:
have := HasDerivedCategory.standard C
  obtain ⟨x, rfl⟩ := x.mk_surjective
  obtain ⟨y, rfl⟩ := y.mk_surjective
  ext
  simp [← CohomologyClass.mk_add, extEquivCohomologyClass_symm_mk_hom, ShiftedHom.map]

Goal state after:
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 : ℕ
y : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) ↑n
this : HasDerivedCategory C
x : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) ↑n
⊢ R.extEquivCohomologyClass.symm (CohomologyClass.mk x + y) =
    R.extEquivCohomologyClass.symm (CohomologyClass.mk x) + R.extEquivCohomologyClass.symm y

Tactic:
obtain ⟨y, rfl⟩ := y.mk_surjective

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
this : HasDerivedCategory C
x y : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) ↑n
⊢ R.extEquivCohomologyClass.symm (CohomologyClass.mk x + CohomologyClass.mk y) =
    R.extEquivCohomologyClass.symm (CohomologyClass.mk x) + R.extEquivCohomologyClass.symm (CohomologyClass.mk y)
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 : ℕ
x y : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) ↑n
⊢ R.extEquivCohomologyClass.symm (x + y) = R.extEquivCohomologyClass.symm x + R.extEquivCohomologyClass.symm y

Tactic:
have := HasDerivedCategory.standard C
  obtain ⟨x, rfl⟩ := x.mk_surjective
  obtain ⟨y, rfl⟩ := y.mk_surjective
  ext
  simp [← CohomologyClass.mk_add, extEquivCohomologyClass_symm_mk_hom, ShiftedHom.map]

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
x y : Pseudoelement P
a a' : Over P
h : pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧
R : C
p : R ⟶ ((fun g ↦ app f g) a).left
q : R ⟶ ((fun g ↦ app f g) a').left
ep : Epi p
w✝¹ : Epi q
comm : p ≫ ((fun g ↦ app f g) a).hom = q ≫ ((fun g ↦ app f g) a').hom
a'' : R ⟶ P := ⋯
Z : C
g : P ⟶ Z
hh : pseudoApply g ⟦a'⟧ = 0
X : C
p' : X ⟶ ((fun g_1 ↦ app g g_1) a').left
q' : X ⟶ (Over.mk 0).left
ep' : Epi p'
w✝ : Epi q'
comm' : p' ≫ ((fun g_1 ↦ app g g_1) a').hom = q' ≫ (Over.mk 0).hom
this : a'.hom ≫ g = 0
⊢ (fun g_1 ↦ app g g_1) (Over.mk a'') ≈ (fun g_1 ↦ app g g_1) a

Tactic:
change app g (a'' : Over P) ≈ app g a

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
x y : Pseudoelement P
a a' : Over P
h : pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧
R : C
p : R ⟶ ((fun g ↦ app f g) a).left
q : R ⟶ ((fun g ↦ app f g) a').left
ep : Epi p
w✝¹ : Epi q
comm : p ≫ ((fun g ↦ app f g) a).hom = q ≫ ((fun g ↦ app f g) a').hom
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
Z : C
g : P ⟶ Z
hh : pseudoApply g ⟦a'⟧ = 0
X : C
p' : X ⟶ ((fun g_1 ↦ app g g_1) a').left
q' : X ⟶ (Over.mk 0).left
ep' : Epi p'
w✝ : Epi q'
comm' : p' ≫ ((fun g_1 ↦ app g g_1) a').hom = q' ≫ (Over.mk 0).hom
this : a'.hom ≫ g = 0
⊢ app g (Over.mk a'') ≈ app g a