mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
this : p - 2 = p - 1 - 1
⊢ 1 / 2 * t ^ (p - 2) = t ^ (p - 1) * (1 / 2 * 1 / t)

Tactic:
rw [this, Real.rpow_sub (by linarith), Real.rpow_one]

Goal state after:
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
this : p - 2 = p - 1 - 1
⊢ 1 / 2 * (t ^ (p - 1) / t) = t ^ (p - 1) * (1 / 2 * 1 / t)
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: m n : ℕ
⊢ eulerMascheroniSeq m < eulerMascheroniSeq' n

Tactic:
have (r : ℕ) : eulerMascheroniSeq r < eulerMascheroniSeq' r := by
    rcases eq_zero_or_pos r with rfl | hr
    · simp [eulerMascheroniSeq, eulerMascheroniSeq']
    simp only [eulerMascheroniSeq, eulerMascheroniSeq', hr.ne', if_false]
    gcongr
    linarith
  apply (strictMono_eulerMascheroniSeq.monotone (le_max_left m n)).trans_lt
  exact (this _).trans_le (strictAnti_eulerMascheroniSeq'.antitone (le_max_right m n))

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ ¬∃ n, s = -(2 * ↑n)

Tactic:
not_exists

Goal state after:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ ∀ (x : ℕ), ¬s = -(2 * ↑x)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: case pos
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s = 1
⊢ (Gammaℝ 1)⁻¹ = Gammaℂ 1 * sin (↑π * 1 / 2) * (1 + 1).Gammaℝ⁻¹

Tactic:
Gammaℝ_one,

Goal state after:
case pos
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s = 1
⊢ 1⁻¹ = Gammaℂ 1 * sin (↑π * 1 / 2) * (1 + 1).Gammaℝ⁻¹
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p : ℝ
hp : p ∈ Ioi 1
s : Set ℝ
hs : s ⊆ Ici 0
⊢ ContinuousOn (Function.uncurry fun t x ↦ t ^ (p - 1) * (t⁻¹ * x + t * (t + x)⁻¹ - 1)) (Ioi 0 ×ˢ s)

Tactic:
fun_prop (disch := grind)

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

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
hg : HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1
⊢ -log ↑π / 2 + (↑√π)⁻¹ * (-↑√π * ((↑γ + 2 * log 2) / 2)) = -(↑γ + log (4 * ↑π)) / 2

Tactic:
← mul_assoc,

Goal state after:
f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
hg : HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1
⊢ -log ↑π / 2 + (↑√π)⁻¹ * -↑√π * ((↑γ + 2 * log 2) / 2) = -(↑γ + log (4 * ↑π)) / 2
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case inl
b : ℕ
hr : 0 ≤ 0
⊢ ⌈logb (↑b) 0⌉ = Int.clog b 0

Tactic:
rw [logb_zero, Int.clog_zero_right, Int.ceil_zero]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
⊢ logb b x = 0 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1

Tactic:
by
  simp_rw [logb, div_eq_zero_iff, log_eq_zero]
  tauto

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
⊢ Integrable (NNReal.toReal ∘ ⇑f) μ

Tactic:
refine ⟨(NNReal.continuous_coe.comp f.continuous).measurable.aestronglyMeasurable, ?_⟩

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
⊢ HasFiniteIntegral (NNReal.toReal ∘ ⇑f) μ
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
⊢ ENNReal.ofReal (∫ (x : ℝ) in Ioc 0 ↑x, x ^ n ∂volume) = ENNReal.ofReal (↑x ^ (n + 1) / (↑n + 1))

pp: n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
⊢ 0 ≤ᵐ[volume.restrict (Ioc 0 ↑x)] fun x ↦ x ^ n

Tactic:
← integral_of_le hr₀

Goal state after:
n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
⊢ ENNReal.ofReal (∫ (x : ℝ) in 0..↑x, x ^ n) = ENNReal.ofReal (↑x ^ (n + 1) / (↑n + 1))

n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
⊢ 0 ≤ᵐ[volume.restrict (Ioc 0 ↑x)] fun x ↦ x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
x : ℂ
⊢ x ∈ L.lattice ↔ ∃ m n, ↑m * L.ω₁ + ↑n * L.ω₂ = x

Tactic:
by
  simp only [lattice, Submodule.mem_span_pair, zsmul_eq_mul]

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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hdim : 1 ≤ Module.finrank ℝ E
f : E → F
C α : ℝ
hα : α < ↑(Module.finrank ℝ E)
h_decay : ∀ᵐ (x : E) ∂μ, ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
⊢ LocallyIntegrable f μ

Tactic:
rw [locallyIntegrable_iff]

Goal state after:
E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hdim : 1 ≤ Module.finrank ℝ E
f : E → F
C α : ℝ
hα : α < ↑(Module.finrank ℝ E)
h_decay : ∀ᵐ (x : E) ∂μ, ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
⊢ ∀ (k : Set E), IsCompact k → IntegrableOn f k μ
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: n : ℕ
a b : Multiset ℂ
hn : n ≠ 0
⊢ ↑n ≠ 0 ∨ ↑(b.card + 1) + (↑a.card - ↑b.card - 1) ≠ 0 ∨ ↑(b.card + 1) = 0 ∧ ↑a.card - ↑b.card - 1 = 0

Tactic:
left; norm_cast

Goal state after:
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) =
    ∑ i ∈ s, deriv (fun x2 ↦ if ↑i = l₀ then 0 else 1 / (x2 - ↑i) ^ 2 - 1 / ↑i ^ 2) l

pp: 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

Tactic:
· congr with x
      split_ifs with hl₁
      · simp
      have hl₁ : l - x ≠ 0 := fun e ↦ hl₁ (by
        obtain rfl := sub_eq_zero.mp e
        simpa using hl)
      rw [deriv_fun_sub (.fun_div (by fun_prop) (by fun_prop) (by simpa)) (by fun_prop),
        deriv_const]
      simp_rw [← zpow_natCast, one_div, ← zpow_neg, Nat.cast_ofNat]
      rw [deriv_comp_sub_const (f := (· ^ (-2 : ℤ))), deriv_zpow]
      simp
      field_simp

Goal state after:
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: case neg
a b : Multiset ℂ
h : a.card = b.card + 1
j : ℂ
hj : j ∈ a
k : ℕ
h' : j = -↑k
⊢ 1 ≤ (regularizedHGFunSeries a b).radius

Tactic:
radius_regularizedHGFunSeries_eq_top_of_finite hj h'

Goal state after:
case neg
a b : Multiset ℂ
h : a.card = b.card + 1
j : ℂ
hj : j ∈ a
k : ℕ
h' : j = -↑k
⊢ 1 ≤ ⊤
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b c : ℂ
⊢ a.regularizedGaussHGFunSeries b c = b.regularizedGaussHGFunSeries a c

Tactic:
unfold regularizedGaussHGFunSeries

Goal state after:
a b c : ℂ
⊢ regularizedHGFunSeries {a, b} {c} = regularizedHGFunSeries {b, a} {c}
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: x : ℝ
hx : 0 < x⁻¹ - 1
⊢ (-log (x⁻¹ - 1)).sigmoid = x

Tactic:
by simp [sigmoid_def, exp_log hx]

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

Goal state before:
pp: f : ℝ → ℝ
hf : ContinuousOn f (Set.Icc (-1) 1)
⊢ Integrable f measureT

Tactic:
replace hf : ContinuousOn f (Set.uIcc (-1) 1) := by rwa [Set.uIcc_of_lt (by norm_num)]

Goal state after:
f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
⊢ Integrable f measureT
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case h₂
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 := ⋯
⊢ Summable (((Function.uncurry fun b c ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b) ∘ ⇑e.symm) ∘ Sum.inr)

Tactic:
dsimp [e, Function.comp_def, Function.uncurry_def, Denumerable.eqv, weierstrassPExceptSummand]

Goal state after:
case h₂
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
⊢ Summable fun x_1 ↦
    (if
          ↑((Equiv.prodCongrLeft fun x ↦
                    { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                      right_inv := ⋯ })
                  (Prod.map some id x_1)).2 =
            l₀ then
        0
      else
        (↑((Equiv.prodCongrLeft fun x ↦
                      { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                        right_inv := ⋯ })
                    (Prod.map some id x_1)).1 +
              1) *
            (↑((Equiv.prodCongrLeft fun x ↦
                        { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                          right_inv := ⋯ })
                      (Prod.map some id x_1)).2 -
                x) ^
              (-(↑((Equiv.prodCongrLeft fun x ↦
                          { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                            right_inv := ⋯ })
                        (Prod.map some id x_1)).1 +
                  2)) -
          Nat.rec
            (↑((Equiv.prodCongrLeft fun x ↦
                      { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                        right_inv := ⋯ })
                    (Prod.map some id x_1)).2 ^
              (-2))
            (fun n n_ih ↦ 0)
            ((Equiv.prodCongrLeft fun x ↦
                  { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
                (Prod.map some id x_1)).1) *
      (z - x) ^
        ((Equiv.prodCongrLeft fun x ↦
              { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
            (Prod.map some id x_1)).1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
this : arcosh x ≠ 0
⊢ 1 < cosh (↑n * arcosh x)

Tactic:
one_lt_cosh,

Goal state after:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
this : arcosh x ≠ 0
⊢ ↑n * arcosh x ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℤ
x : ℝ
hx : x ≤ -1
⊢ (-1) ^ n * ((-1) ^ n * eval (-x) (T ℝ n)) = eval (-x) (T ℝ n)

Tactic:
← mul_assoc,

Goal state after:
n : ℤ
x : ℝ
hx : x ≤ -1
⊢ (-1) ^ n * (-1) ^ n * eval (-x) (T ℝ n) = eval (-x) (T ℝ n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case refine_1
n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ (-1) ^ i * (↑k.factorial * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹)

Tactic:
← mul_assoc,

Goal state after:
case refine_1
n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ (-1) ^ i * ↑k.factorial * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℤ
hn : n ≠ 0
x : ℝ
hx : x < -1
⊢ (-1) ^ n * ((-1) ^ n * eval (-x) (T ℝ n)) = eval (-x) (T ℝ n)

Tactic:
← mul_assoc,

Goal state after:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : x < -1
⊢ (-1) ^ n * (-1) ^ n * eval (-x) (T ℝ n) = eval (-x) (T ℝ n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case refine_1
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 < (-1) ^ i * (↑k.factorial * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹)

Tactic:
← mul_assoc,

Goal state after:
case refine_1
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 < (-1) ^ i * ↑k.factorial * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case pos
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
⊢ 0 ^ (-k) ≤ r z ^ (-k) * 0 ^ (-k)

Tactic:
by_cases h : -k = 0

Goal state after:
case pos
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
h : -k = 0
⊢ 0 ^ (-k) ≤ r z ^ (-k) * 0 ^ (-k)

case neg
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
h : ¬-k = 0
⊢ 0 ^ (-k) ≤ r z ^ (-k) * 0 ^ (-k)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
a b : ℤ
⊢ (fun m ↦ ((↑(m 0) + ↑a) * ↑z + ↑(m 1) + ↑b)⁻¹) =O[cofinite] fun m ↦ ‖![m 0 + a, m 1 + b]‖⁻¹

Tactic:
by
  rw [Asymptotics.isBigO_iff]
  have h0 : z ∈ verticalStrip |z.re| (z.im) := by simp [mem_verticalStrip_iff]
  use ‖r ⟨⟨|z.re|, z.im⟩, z.2⟩‖⁻¹
  filter_upwards with m
  apply le_trans (by simpa [Real.rpow_neg_one, add_assoc] using
    summand_bound_of_mem_verticalStrip zero_le_one ![m 0 + a, m 1 + b] z.2 h0)
  simp [abs_of_pos (r_pos _)]

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

Goal state before:
pp: case succ
R : Type u_1
a b u₀ : R
inst✝ : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
⊢ a * (a ^ n * u₀) + a * (b * ∑ k ∈ Finset.range n, a ^ k) + b =
    a ^ (n + 1) * u₀ + b * ∑ k ∈ Finset.range (n + 1), a ^ k

Tactic:
← mul_assoc,

Goal state after:
case succ
R : Type u_1
a b u₀ : R
inst✝ : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
⊢ a * a ^ n * u₀ + a * (b * ∑ k ∈ Finset.range n, a ^ k) + b = a ^ (n + 1) * u₀ + b * ∑ k ∈ Finset.range (n + 1), a ^ k
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this : (⇑derivative)^[k] (T ℝ ↑n) ∈ Submodule.span ℕ ((fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k))
f : ℝ[X] →₀ ℕ
hfsupp : ↑f.support ⊆ (fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k)
hfderiv : (f.sum fun mi r ↦ r • mi) = (⇑derivative)^[k] (T ℝ ↑n)
⊢ ∑ p ∈ f.support, f p • p = (⇑derivative)^[k] (T ℝ ↑n)

Tactic:
rw [← hfderiv]

Goal state after:
k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this : (⇑derivative)^[k] (T ℝ ↑n) ∈ Submodule.span ℕ ((fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k))
f : ℝ[X] →₀ ℕ
hfsupp : ↑f.support ⊆ (fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k)
hfderiv : (f.sum fun mi r ↦ r • mi) = (⇑derivative)^[k] (T ℝ ↑n)
⊢ ∑ p ∈ f.support, f p • p = f.sum fun mi r ↦ r • mi
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
| Summable fun i ↦ ‖(↑i + 1) ^ (-1 - ↑k)‖

Tactic:
enter [1, n]

Goal state after:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
n : ℕ
| ‖(↑n + 1) ^ (-1 - ↑k)‖
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: this : fibRec.IsSolution ((fun n ↦ (√5)⁻¹ * φ ^ n) - fun n ↦ (√5)⁻¹ * ψ ^ n)
⊢ fibRec.IsSolution fun n ↦ (φ ^ n - ψ ^ n) / √5

Tactic:
convert! this
      rw [Pi.sub_apply]
      ring

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

Goal state before:
pp: case hf
n l : ℕ
x : ℂ
hx : x ∈ ℍₒ
⊢ x + (↑n + 1) ≠ 0

Tactic:
simpa [add_eq_zero_iff_neg_eq'] using (UpperHalfPlane.ne_intCast (.mk x hx) (-(n + 1))).symm

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
integrable : IntegrableOn f (Ioi ↑N) volume
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
M : ℕ
⊢ ∑ i ∈ Finset.range M, f ↑(i + (N + 1)) ≤ ∫ (t : ℝ) in Ioi ↑N, f t

Tactic:
calc
    _ = ∑ n ∈ Finset.Ico N (N + M), f (n + 1 : ℕ) := by rw [Finset.sum_Ico_eq_sum_range]; grind
    _ ≤ _ := (anti.mono Icc_subset_Ici_self).sum_Ico_le_integral integrable nonneg

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 ^ 2)⁻¹ * c) ≤ c ^ 2

Tactic:
← mul_assoc,

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 ^ 2)⁻¹ * c ≤ c ^ 2
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.left ⟶
    (mk { left := Z.left.hom, right := Z.right.hom, w := ⋯ }).right.left

Tactic:
exact f.left.right

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Indization.Category

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type v
inst✝¹ : Finite α
inst✝ : HasColimitsOfShape (Discrete α) C
F : Discrete α ⥤ Ind C
I : α → Type v := fun s ↦ (F.obj { as := s }).presentation.I
G : (s : α) → I s ⥤ C := fun s ↦ (F.obj { as := s }).presentation.F
⊢ HasColimit F

Tactic:
let iso : Discrete.functor (fun s => Pi.eval I s ⋙ G s) ⋙
      (whiskeringRight _ _ _).obj Ind.yoneda ⋙ colim ≅ F := by
    refine Discrete.natIso (fun s => ?_)
    refine (Functor.Final.colimitIso (Pi.eval I s.as) (G s.as ⋙ Ind.yoneda)) ≪≫ ?_
    exact Ind.colimitPresentationCompYoneda _

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
α : Type v
inst✝¹ : Finite α
inst✝ : HasColimitsOfShape (Discrete α) C
F : Discrete α ⥤ Ind C
I : α → Type v := fun s ↦ (F.obj { as := s }).presentation.I
G : (s : α) → I s ⥤ C := fun s ↦ (F.obj { as := s }).presentation.F
iso : (Discrete.functor fun s ↦ Pi.eval I s ⋙ G s) ⋙
    (whiskeringRight ((i : α) → I i) C (Ind C)).obj Ind.yoneda ⋙ colim ≅
  F :=
  Discrete.natIso fun s ↦
    Final.colimitIso (Pi.eval I s.as) (G s.as ⋙ Ind.yoneda) ≪≫ (F.obj { as := s.as }).colimitPresentationCompYoneda
⊢ HasColimit F
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
α : { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ } ⟶
  { X₁ := X, X₂ := Y, X₃ := syzygies f, f := f, g := d f, zero := ⋯ } :=
  { τ₁ := 𝟙 { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁,
    τ₂ := 𝟙 { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂,
    τ₃ := ι { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.Exact

Tactic:
apply ShortComplex.exact_of_g_is_cokernel

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
α : { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ } ⟶
  { X₁ := X, X₂ := Y, X₃ := syzygies f, f := f, g := d f, zero := ⋯ } := ⋯
⊢ IsColimit (CokernelCofork.ofπ { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.g ⋯)
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 : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
p : ℕ
hp : p + 1 = n
⊢ R.extMk f m hm hf = 0 ↔ ∃ g, g ≫ R.cocomplex.d p n = f

Tactic:
simp only [← R.extEquivCohomologyClass.apply_eq_iff_eq,
    extEquivCohomologyClass_extMk, extEquivCohomologyClass_zero,
    CohomologyClass.mk_eq_zero_iff]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
p : ℕ
hp : p + 1 = n
⊢ Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯ ∈
      coboundaries ((singleFunctor C 0).obj X) R.cochainComplex ↑n ↔
    ∃ g, g ≫ R.cocomplex.d p n = f
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
⊢ IsTrans (Over P) (PseudoEqual P)

Tactic:
by
  refine ⟨fun f g h ⟨R, p, q, ep, Eq, comm⟩ ⟨R', p', q', ep', eq', comm'⟩ ↦ ?_⟩
  refine ⟨pullback q p', pullback.fst _ _ ≫ p, pullback.snd _ _ ≫ q',
    epi_comp _ _, epi_comp _ _, ?_⟩
  rw [Category.assoc, comm, ← Category.assoc, pullback.condition, Category.assoc, comm',
    Category.assoc]

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
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0

Tactic:
by
      -- If we apply `g` to the pseudoelement induced by its kernel, we get 0 (of course!).
      have : S.g (kernel.ι S.g) = 0 := apply_eq_zero_of_comp_eq_zero _ _ (kernel.condition _)
      -- By pseudo-exactness, we get a preimage.
      obtain ⟨a', ha⟩ := hS _ this
      obtain ⟨a, ha'⟩ := Quotient.exists_rep a'
      rw [← ha'] at ha
      obtain ⟨Z, r, q, _, eq, comm⟩ := Quotient.exact ha
      -- Consider the pullback of `kernel.ι (cokernel.π f)` and `kernel.ι g`.
      -- The commutative diagram given by the pseudo-equality `f a = b` induces
      -- a cone over this pullback, so we get a factorization `z`.
      obtain ⟨z, _, hz₂⟩ := @pullback.lift' _ _ _ _ _ _ (kernel.ι (cokernel.π S.f))
        (kernel.ι S.g) _ (r ≫ a.hom ≫ Abelian.factorThruImage S.f) q (by
          simp only [Category.assoc, Abelian.image.fac]
          exact comm)
      -- Let's give a name to the second pullback morphism.
      let j : pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ⟶ kernel S.g := pullback.snd _ _
      -- Since `q` is an epimorphism, in particular this means that `j` is an epimorphism.
      have pe : Epi j := epi_of_epi_fac hz₂
      -- But it is also a monomorphism, because `kernel.ι (cokernel.π f)` is: A kernel is
      -- always a monomorphism and the pullback of a monomorphism is a monomorphism.
      -- But mono + epi = iso, so `j` is an isomorphism.
      have : IsIso j := isIso_of_mono_of_epi _
      -- But then `kernel.ι g` can be expressed using all of the maps of the pullback square, and we
      -- are done.
      rw [(Iso.eq_inv_comp (asIso j)).2 pullback.condition.symm]
      simp only [Category.assoc, kernel.condition, HasZeroMorphisms.comp_zero]

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 : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
p : ℕ
hp : p + 1 = n
⊢ R.extMk f m hm hf = 0 ↔ ∃ g, R.complex.d n p ≫ g = f

Tactic:
simp only [← R.extEquivCohomologyClass.apply_eq_iff_eq,
    extEquivCohomologyClass_extMk, extEquivCohomologyClass_zero,
    CohomologyClass.mk_eq_zero_iff]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
p : ℕ
hp : p + 1 = n
⊢ Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯ ∈
      coboundaries R.cochainComplex ((singleFunctor C 0).obj Y) ↑n ↔
    ∃ g, R.complex.d n p ≫ g = f