mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: case inr.hsup
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
key : ‖f‖ - ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ‖f‖ - ∫ (x : X), f x ∂μs i) L
this : liminf (fun i ↦ ‖f‖ - ∫ (x : X), f x ∂μs i) L = ‖f‖ - limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L
⊢ limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ

Tactic:
this,

Goal state after:
case inr.hsup
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
key : ‖f‖ - ∫ (x : X), f x ∂μ ≤ ‖f‖ - limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L
this : liminf (fun i ↦ ‖f‖ - ∫ (x : X), f x ∂μs i) L = ‖f‖ - limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L
⊢ limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
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
obs : ∀ (x : ℝ), ∫ (t : ℝ) in 0..x, t ^ (p - 1) = x ^ p / p
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))

Tactic:
set g := fun t : ℝ => t ^ (p - 1)

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
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
s : Set ↑(sphere 0 1)
hs : s ∈ {s | MeasurableSet s}
r : ↑(Ioi 0)
this : Ioo 0 ↑r = ↑r • Ioo 0 1
hpos : 0 < dim E
⊢ μ (Ioo 0 ↑r • Subtype.val '' s) =
    ↑(dim E) * μ (Ioo 0 1 • Subtype.val '' s) * ENNReal.ofReal (↑r ^ (dim E - 1 + 1) / (↑(dim E - 1) + 1))

Tactic:
this,

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
a✝ : Nontrivial E
s : Set ↑(sphere 0 1)
hs : s ∈ {s | MeasurableSet s}
r : ↑(Ioi 0)
this : Ioo 0 ↑r = ↑r • Ioo 0 1
hpos : 0 < dim E
⊢ μ ((↑r • Ioo 0 1) • Subtype.val '' s) =
    ↑(dim E) * μ (Ioo 0 1 • Subtype.val '' s) * ENNReal.ofReal (↑r ^ (dim E - 1 + 1) / (↑(dim E - 1) + 1))
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    IntegrableOn (fun y ↦ y ^ (dim E - 1) • f y) (Ioi 0) volume

Tactic:
this,

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1))) ↔
    IntegrableOn (fun y ↦ y ^ (dim E - 1) • f y) (Ioi 0) volume
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: ⊢ Continuous sigmoid

Tactic:
apply Differentiable.continuous (𝕜 := ℝ)

Goal state after:
⊢ Differentiable ℝ sigmoid
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case pos
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∈ L.lattice
this : ℘[L - z + ↑l] (z + ↑l) = ℘[L - z + ↑l - ↑l] z + (1 / (z + ↑l) ^ 2 - 1 / (z + ↑l - ↑l) ^ 2)
⊢ ℘[L - ↑⟨z + ↑l, ⋯⟩] (z + ↑l) + (1 / (z + ↑l - ↑⟨z + ↑l, ⋯⟩) ^ 2 - 1 / ↑⟨z + ↑l, ⋯⟩ ^ 2) = ℘[L] z

Tactic:
this,

Goal state after:
case pos
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∈ L.lattice
this : ℘[L - z + ↑l] (z + ↑l) = ℘[L - z + ↑l - ↑l] z + (1 / (z + ↑l) ^ 2 - 1 / (z + ↑l - ↑l) ^ 2)
⊢ ℘[L - z + ↑l - ↑l] z + (1 / (z + ↑l) ^ 2 - 1 / (z + ↑l - ↑l) ^ 2) +
      (1 / (z + ↑l - ↑⟨z + ↑l, ⋯⟩) ^ 2 - 1 / ↑⟨z + ↑l, ⋯⟩ ^ 2) =
    ℘[L] z
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∉ L.lattice
this : ℘[L - 0] (z + ↑l) = ℘[L - -↑l] z + -(↑l ^ 2)⁻¹
⊢ ℘[L - 0] (z + ↑l) + (1 / (z + ↑l - 0) ^ 2 - 1 / 0 ^ 2) = ℘[L] z

Tactic:
this,

Goal state after:
case neg
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∉ L.lattice
this : ℘[L - 0] (z + ↑l) = ℘[L - -↑l] z + -(↑l ^ 2)⁻¹
⊢ ℘[L - -↑l] z + -(↑l ^ 2)⁻¹ + (1 / (z + ↑l - 0) ^ 2 - 1 / 0 ^ 2) = ℘[L] z
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case l₂
| 𝓝 (1 / 2)

Tactic:
rw [one_div, ← add_zero (2 : ℝ)]

Goal state after:
case l₂
| 𝓝 (2 + 0)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ (↑n ! / (√(2 * ↑n) * (↑n / rexp 1) ^ n)) ^ 4 / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1)) = Wallis.W n

Tactic:
this,

Goal state after:
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ (↑n ! / (√(2 * ↑n) * (↑n / rexp 1) ^ n)) ^ (2 * 2) / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1)) = Wallis.W n
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: 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 !

Tactic:
this,

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.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
this : ∫ (θ : ℝ) in 0..↑n * π, cos θ = 0
⊢ (↑n)⁻¹ • ∫ (x : ℝ) in ↑n * 0..↑n * π, cos x = 0

Tactic:
smul_eq_zero_iff_right (by aesop),

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

Goal state before:
pp: case inr
n i : ℕ
hi : i ∈ Finset.Iic n
hn : n ≠ 0
this : ↑↑n * (↑i * π / ↑n) = ↑i * π
⊢ cos (↑↑n * (↑i * π / ↑n)) = (-1) ^ i

Tactic:
this,

Goal state after:
case inr
n i : ℕ
hi : i ∈ Finset.Iic n
hn : n ≠ 0
this : ↑↑n * (↑i * π / ↑n) = ↑i * π
⊢ cos (↑i * π) = (-1) ^ i
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: 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
hf : ∀ {s a b t : ℂ}, s * a⁻¹ * b = t → a ≠ 0 → b ≠ 0 → s = a / b * t
⊢ Complex.exp (↑k / ↑n * ↑π * I) - 1 ≠ 0

Tactic:
by grind [exp_sub_one_ne_zero]

Goal state after:
Module: Mathlib.NumberTheory.Niven

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

Tactic:
by
    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.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: case inr
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : (-1) ^ (-k) = (-1) ^ k
⊢ Complex.exp (↑k / (2 * ↑n) * ↑π * I) / (Complex.exp (↑k / ↑n * ↑π * I) - 1) * ((-1) ^ k - 1) +
      (Complex.exp (↑k / (2 * ↑n) * ↑π * I))⁻¹ / ((Complex.exp (↑k / ↑n * ↑π * I))⁻¹ - 1) * ((-1) ^ (-k) - 1) =
    0

Tactic:
this,

Goal state after:
case inr
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : (-1) ^ (-k) = (-1) ^ k
⊢ Complex.exp (↑k / (2 * ↑n) * ↑π * I) / (Complex.exp (↑k / ↑n * ↑π * I) - 1) * ((-1) ^ k - 1) +
      (Complex.exp (↑k / (2 * ↑n) * ↑π * I))⁻¹ / ((Complex.exp (↑k / ↑n * ↑π * I))⁻¹ - 1) * ((-1) ^ k - 1) =
    0
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : LocallyFiniteOrder α
⊢ Monotone fun n ↦ Icc (-↑n) ↑n

Tactic:
refine fun m n hmn ↦ by apply Icc_subset_Icc <;> simpa using Nat.mono_cast hmn

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
n : ℕ
inst✝ : DecidableEq α
x : α
hx : x ∈ box n
hn : n = 0
⊢ x = 0

Tactic:
by rwa [hn, box_zero, mem_singleton] at hx

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: x : ℤ × ℤ
⊢ ∃! n, x ∈ box n

Tactic:
use max x.1.natAbs x.2.natAbs; simp only [mem_box, and_self_iff, forall_eq']

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

Goal state before:
pp: c d : ℝ
hc : 1 ≤ c ^ 2
z : ℂ
hz : 0 < z.im
⊢ z.im ^ 2 ≤ (c * z.re + d) ^ 2 + c ^ 2 * z.im ^ 2

Tactic:
exact (le_mul_of_one_le_left (sq_nonneg _) hc).trans <| le_add_of_nonneg_left (sq_nonneg _)

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

Goal state before:
pp: n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
⊢ arcosh x ≠ 0

Tactic:
grind [cosh_arcosh, cosh_zero]

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

Goal state before:
pp: n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ IsLocalMax (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n))

Tactic:
refine eventually_nhds_iff.mpr ⟨Set.Ioo (-1) 1, ?_, isOpen_Ioo, ?_, ?_⟩

Goal state after:
case refine_1
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ ∀ y ∈ Set.Ioo (-1) 1, (fun x ↦ eval x (T ℝ ↑n)) y ≤ (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n))

case refine_2
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ -1 < cos (↑k * π / ↑n)

case refine_3
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ cos (↑k * π / ↑n) < 1
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: α : Type u_1
a : α
inst✝² : NormedAddCommGroup α
inst✝¹ : DiscreteTopology α
inst✝ : ProperSpace α
⊢ (fun x ↦ a) =o[cofinite] fun x ↦ ‖x‖

Tactic:
simpa [isLittleO_const_left, Function.comp_def] using
    .inr <| tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding IsClosedEmbedding.id

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

Goal state before:
pp: n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ IsLocalMin (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n))

Tactic:
refine eventually_nhds_iff.mpr ⟨Set.Ioo (-1) 1, ?_, isOpen_Ioo, ?_, ?_⟩

Goal state after:
case refine_1
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ ∀ y ∈ Set.Ioo (-1) 1, (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n)) ≤ (fun x ↦ eval x (T ℝ ↑n)) y

case refine_2
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ -1 < cos (↑k * π / ↑n)

case refine_3
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ cos (↑k * π / ↑n) < 1
Module: Mathlib.Data.Int.Fib.Basic

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

Tactic:
this,

Goal state after:
case inl
n : ℕ
hn0 : ¬n + n = 0
this : -↑(n + n) + 1 = -↑(n + n - 1)
⊢ (-1) ^ (n + n + 1) * (↑(Nat.fib (n + n)) - ↑(Nat.fib (n + n - 1) + Nat.fib (n + n))) = fib (-↑(n + n - 1))
Module: Mathlib.Data.Int.Fib.Basic

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

Tactic:
this,

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

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ logDeriv (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) x = ↑π * (↑π * x).cot - 1 / x

Tactic:
this,

Goal state after:
x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ logDeriv (fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)) x = ↑π * (↑π * x).cot - 1 / x
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case inl
n : ℕ
⊢ fib ↑n = 0 ↔ ↑n = 0

Tactic:
simp [fib_neg_natCast]

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

Goal state before:
pp: case inr
n : ℕ
⊢ fib (-↑n) = 0 ↔ -↑n = 0

Tactic:
simp [fib_neg_natCast]

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

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∑ i ∈ Finset.range n, logDeriv (fun z ↦ 1 + sineTerm z i) x = ∑ j ∈ Finset.range n, cotTerm x j

pp: case hf
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∀ i ∈ Finset.range n, 1 + sineTerm x i ≠ 0

pp: case hd
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∀ i ∈ Finset.range n, DifferentiableAt ℂ (fun z ↦ 1 + sineTerm z i) x

Tactic:
· simp_rw [logDeriv_sineTerm_eq_cotTerm hx]

Goal state after:
case hf
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∀ i ∈ Finset.range n, 1 + sineTerm x i ≠ 0

case hd
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∀ i ∈ Finset.range n, DifferentiableAt ℂ (fun z ↦ 1 + sineTerm z i) x
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case refine_1
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 < ε
⊢ ∀ᶠ (b : ℕ) in atTop, d < u b / ↑b

Tactic:
filter_upwards [B ε εpos, Ioi_mem_atTop 0] with n hn npos

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
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 < u n / ↑n
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
hN : 1 ≤ N
anti : AntitoneOn f (Ici (↑N - 1))
integrable : IntegrableOn f (Ioi (↑N - 1)) volume
nonneg : ∀ t ∈ Ioi (↑N - 1), 0 ≤ f t
⊢ |∑' (i : ℕ), f ↑(i + N)| ≤ ∫ (x : ℝ) in Ioi (↑N - 1), f x

Tactic:
abs_of_nonneg (tsum_nonneg <| by grind)

Goal state after:
f : ℝ → ℝ
N : ℕ
hN : 1 ≤ N
anti : AntitoneOn f (Ici (↑N - 1))
integrable : IntegrableOn f (Ioi (↑N - 1)) volume
nonneg : ∀ t ∈ Ioi (↑N - 1), 0 ≤ f t
⊢ ∑' (i : ℕ), f ↑(i + N) ≤ ∫ (x : ℝ) in Ioi (↑N - 1), f x
Module: Mathlib.CategoryTheory.Filtered.Small

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

Tactic:
refine ⟨⟨0, ?_⟩, ?_⟩
      · simp only [FilteredClosureSmall.bundledAbstractFilteredClosure]
        exact ULift.up x
      · simp only [FilteredClosureSmall.abstractFilteredClosureRealization,
          FilteredClosureSmall.bundledAbstractFilteredClosure]
        rfl

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
ι : Type u_2
inst✝⁵ : HasProductsOfShape ι C
inst✝⁴ : IsIPCOfShape.{w, u_2, v_1, u_1} ι C
J : ι → Type w
inst✝³ : (i : ι) → SmallCategory (J i)
inst✝² : ∀ (i : ι), IsFiltered (J i)
F : (i : ι) → J i ⥤ C
inst✝¹ : ∀ (i : ι), HasColimit (F i)
inst✝ : HasColimit (pointwiseProduct F)
⊢ IsIso (colimitPointwiseProductToProductColimit F)

Tactic:
by
  rw [colimitPointwiseProductToProductColimit, colimit.desc]
  refine ((colimit.isColimit (pointwiseProduct F)).nonempty_isColimit_iff_isIso_desc).mp ?_
  exact IsIPCOfShape.nonempty_isColimit fun i ↦ colimit.isColimit _

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected

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

Tactic:
have := hc.isIso_colimMap_ι

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
R : InjectiveResolution X
⊢ R.cochainComplex.IsLE 0

Tactic:
simp only [← HomologicalComplex.isSupported_iff_of_quasiIso R.ι']
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b
this✝ : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0
a' : Pseudoelement S.X₁
a : Over S.X₁
ha : pseudoApply S.f ⟦a⟧ = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))
ha' : ⟦a⟧ = a'
Z : C
r : Z ⟶ ((fun g ↦ app S.f g) a).left
q : Z ⟶ (Over.mk (kernel.ι S.g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g ↦ app S.f g) a).hom = q ≫ (Over.mk (kernel.ι S.g)).hom
z : Z ⟶ pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)
left✝ : z ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = r ≫ a.hom ≫ Abelian.factorThruImage S.f
hz₂ : z ≫ pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = q
j : pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ⟶ kernel S.g :=
  pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)
pe : Epi j
this : IsIso j
⊢ ((asIso j).inv ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ≫ kernel.ι (cokernel.π S.f)) ≫
      cokernel.π S.f =
    0

Tactic:
simp only [Category.assoc, kernel.condition, HasZeroMorphisms.comp_zero]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
P : ObjectProperty C
inst✝¹ : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ P.isoModSerre f ↔ P.epiModSerre f

Tactic:
by
  have := P.monoModSerre_of_mono f
  rw [isoModSerre_iff]
  tauto

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

Goal state before:
pp: case refine_1
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' : ↑x.left
ha' : (ModuleCat.Hom.hom x.hom) a' = a
⊢ a ∈ (ModuleCat.Hom.hom y.hom).range

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

Goal state after:
case refine_1
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' : ↑x.left
ha' : (ModuleCat.Hom.hom x.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom p) a'' = a'
⊢ a ∈ (ModuleCat.Hom.hom y.hom).range
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
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝ : L.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
tfae_2_to_3 : P.epiModSerre f → ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ (L.objObjPreimageIso W).inv = φ.map L ⋯
this : L.map φ.f = z ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s
⊢ L.map f ≫ L.map φ.f = 0

Tactic:
this,

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
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝ : L.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
tfae_2_to_3 : P.epiModSerre f → ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ (L.objObjPreimageIso W).inv = φ.map L ⋯
this : L.map φ.f = z ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s
⊢ L.map f ≫ z ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s = 0