mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ (2.7182818286 ^ (107 / 60)) ^ 60 < 6 ^ 60

pp: case hx
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 2.7182818286 ^ (107 / 60)

pp: case hy
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 6

pp: case hz
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 < 60

Tactic:
← rpow_mul,

Goal state after:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 2.7182818286 ^ (107 / 60 * 60) < 6 ^ 60

case hx
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 2.7182818286

case hx
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 2.7182818286 ^ (107 / 60)

case hy
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 6

case hz
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 < 60
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: n : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
x : ℝ
hx : 0 < x
⊢ deriv f (x + 1) = deriv f x + 1 / x

Tactic:
← deriv_comp_add_const,

Goal state after:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
x : ℝ
hx : 0 < x
⊢ deriv (fun x ↦ f (x + 1)) x = deriv f x + 1 / x
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ (fun x ↦ cexp (a * ↑x ^ 2 + b * ↑x)) =o[atTop] fun x ↦ x ^ s

Tactic:
apply Asymptotics.IsLittleO.of_norm_left
  convert! rexp_neg_quadratic_isLittleO_rpow_atTop ha b.re s with x
  simp_rw [Complex.norm_exp, add_re, ← ofReal_pow, mul_comm (_ : ℂ) ↑(_ : ℝ),
      re_ofReal_mul, mul_comm _ (re _)]

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

Goal state before:
pp: case e_a.e_a.e_a
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ deriv (Gamma ∘ fun s ↦ 2 * s) (1 / 2) = -2 * γ

Tactic:
rw [deriv_comp, deriv_const_mul_id, mul_one_div, div_self two_ne_zero]

Goal state after:
case e_a.e_a.e_a
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ deriv Gamma 1 * 2 = -2 * γ

case e_a.e_a.e_a.hh₂
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ Gamma (2 * (1 / 2))

case e_a.e_a.e_a.hh
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ (fun s ↦ 2 * s) (1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b c : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
⊢ ¬c = 0 → Tendsto (Norm.norm ∘ logb b) atTop atTop

Tactic:
intro hc

Goal state after:
b c : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hc : ¬c = 0
⊢ Tendsto (Norm.norm ∘ logb b) atTop atTop
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
this : ∀ (n : ℕ), ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
x : ℝ
hx : x ≥ x₀
hx' : 0 < x / x₀
⊢ x₀ ≤ x ∧ logb r (x / x₀) < ↑⌊logb r (x / x₀)⌋₊ + 1

Tactic:
exact ⟨hx, Nat.lt_floor_add_one _⟩

Goal state after:
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

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

Tactic:
rcases ENNReal.exists_pos_sum_of_countable' (ne_of_gt hε) ℕ with ⟨δ, hδ1, hδ2⟩

Goal state after:
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
a✝ : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
s' : ℕ → ℝ≥0∞ → ℕ
s'bound : ∀ (n : ℕ) (ε : ℝ≥0∞), 0 < ε → P (⋂ m', ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε
δ : ℕ → ℝ≥0∞
hδ1 : ∀ (i : ℕ), 0 < δ i
hδ2 : ∑' (i : ℕ), δ i < ε
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: case succ
n a fuel : ℕ
ih : ∀ {guess : ℕ}, guess ≤ fuel → go n a fuel guess ^ (n + 2) ≤ a
guess : ℕ
hle : guess ≤ fuel + 1
⊢ (if (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess then
        go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2))
      else guess) ^
      (n + 2) ≤
    a

Tactic:
split_ifs with h

Goal state after:
case pos
n a fuel : ℕ
ih : ∀ {guess : ℕ}, guess ≤ fuel → go n a fuel guess ^ (n + 2) ≤ a
guess : ℕ
hle : guess ≤ fuel + 1
h : (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
⊢ go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2)) ^ (n + 2) ≤ a

case neg
n a fuel : ℕ
ih : ∀ {guess : ℕ}, guess ≤ fuel → go n a fuel guess ^ (n + 2) ≤ a
guess : ℕ
hle : guess ≤ fuel + 1
h : ¬(a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
⊢ guess ^ (n + 2) ≤ a
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: n : ℕ
ε : ℝ
⊢ 0 < if n ≠ 0 ∧ 0 < ε then ↑n * (min ε.toNNReal 2 / 4) ^ n else 1

Tactic:
split_ifs with h

Goal state after:
case pos
n : ℕ
ε : ℝ
h : n ≠ 0 ∧ 0 < ε
⊢ 0 < ↑n * (min ε.toNNReal 2 / 4) ^ n

case neg
n : ℕ
ε : ℝ
h : ¬(n ≠ 0 ∧ 0 < ε)
⊢ 0 < 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: case succ
n a fuel : ℕ
ih : ∀ {guess : ℕ}, a < (guess + 1) ^ (n + 2) → a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
⊢ a <
    ((if (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess then
          go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2))
        else guess) +
        1) ^
      (n + 2)

Tactic:
split_ifs with h

Goal state after:
case pos
n a fuel : ℕ
ih : ∀ {guess : ℕ}, a < (guess + 1) ^ (n + 2) → a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
h : (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
⊢ a < (go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2)) + 1) ^ (n + 2)

case neg
n a fuel : ℕ
ih : ∀ {guess : ℕ}, a < (guess + 1) ^ (n + 2) → a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
h : ¬(a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
⊢ a < (guess + 1) ^ (n + 2)
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
r : ℝ
⊢ Integrable ((ball 0 r).indicator fun x ↦ f ‖x‖) μ ↔ Integrable (fun x ↦ (Iio r).indicator f ‖x‖) μ

Tactic:
apply integrable_congr

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
r : ℝ
⊢ ((ball 0 r).indicator fun x ↦ f ‖x‖) =ᵐ[μ] fun x ↦ (Iio r).indicator f ‖x‖
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: x : ℝ
⊢ (-x).sigmoid = 1 - x.sigmoid

Tactic:
by
  simp only [sigmoid_def]
  field_simp
  simp [add_mul, ← Real.exp_add, add_comm (1 : ℝ)]

Goal state after:
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
r x : ℝ
hx : 0 < x
⊢ (fun y ↦ y ^ (dim E - 1) • (Iio r).indicator f y) x = (Ioo 0 r).indicator (fun y ↦ y ^ (dim E - 1) • f y) x

Tactic:
by_cases hxr : x < r

Goal state after:
case pos
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
r x : ℝ
hx : 0 < x
hxr : x < r
⊢ (fun y ↦ y ^ (dim E - 1) • (Iio r).indicator f y) x = (Ioo 0 r).indicator (fun y ↦ y ^ (dim E - 1) • f y) x

case neg
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
r x : ℝ
hx : 0 < x
hxr : ¬x < r
⊢ (fun y ↦ y ^ (dim E - 1) • (Iio r).indicator f y) x = (Ioo 0 r).indicator (fun y ↦ y ^ (dim E - 1) • f y) x
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
⊢ (μ.toSphere.real univ •
      ∫ (x : ↑(Ioi 0)), f ↑x ∂(Measure.comap Subtype.val volume).withDensity fun r ↦ ↑(↑r ^ (dim E - 1)).toNNReal) =
    dim E • μ.real (ball 0 1) • ∫ (y : ℝ) in Ioi 0, y ^ (dim E - 1) • f y

Tactic:
rw [integral_withDensity_eq_integral_smul, μ.toSphere_real_apply_univ,
        ← nsmul_eq_mul, smul_assoc,
        integral_subtype_comap measurableSet_Ioi fun a ↦ Real.toNNReal (a ^ (dim E - 1)) • f a,
        setIntegral_congr_fun measurableSet_Ioi fun x hx ↦ ?_]

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
x : ℝ
hx : x ∈ Ioi 0
⊢ (x ^ (dim E - 1)).toNNReal • f x = x ^ (dim E - 1) • f x

case f_meas
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
⊢ Measurable fun r ↦ (↑r ^ (dim E - 1)).toNNReal
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ (℘'[L - ↑l₀] z + ∑' (i : ↥L.lattice), if ↑i = ↑l₀ then -2 / (z - ↑l₀) ^ 3 else 0) = ℘'[L] z

Tactic:
derivWeierstrassP,

Goal state after:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ (℘'[L - ↑l₀] z + ∑' (i : ↥L.lattice), if ↑i = ↑l₀ then -2 / (z - ↑l₀) ^ 3 else 0) =
    -∑' (l : ↥L.lattice), 2 / (z - ↑l) ^ 3
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a

Tactic:
rcases hab.eq_or_lt with rfl | h'ab

Goal state after:
case inl
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a a)
hab : a ≤ a
⊢ ∫ (x : ℝ) in a..a, deriv f x = f a - f a

case inr
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l : ↥L.lattice
⊢ ℘'[L] ↑l = 0

Tactic:
by
  rw [← zero_add l.1, L.derivWeierstrassP_add_coe, L.derivWeierstrassP_zero]

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

Goal state before:
pp: n : ℕ
r : ℝ := (1 / (2 * (↑n + 1) + 1)) ^ 2
hr : r = (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ r < 1

Tactic:
grw [hr, ← n.zero_le]

Goal state after:
n : ℕ
r : ℝ := (1 / (2 * (↑n + 1) + 1)) ^ 2
hr : r = (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ (1 / (2 * (↑0 + 1) + 1)) ^ 2 < 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: ⊢ ∫ (x : ℝ), eval x (T ℝ 0 * T ℝ 0) ∂measureT = π

Tactic:
show (T ℝ 0) * (T ℝ 0) = T ℝ 0 by simp

Goal state after:
⊢ ∫ (x : ℝ), eval x (T ℝ 0) ∂measureT = π
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case e_f
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
l : ↥L.lattice
⊢ (if ↑l = l₀ then 0 else 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2) =
    ∑' (i : ℕ), if ↑l = l₀ then 0 else ((↑i + 1) * (↑l - x) ^ (-↑(i + 2)) - Nat.casesOn i (↑l ^ (-2)) 0) * (z - x) ^ i

Tactic:
split_ifs with h

Goal state after:
case pos
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
l : ↥L.lattice
h : ↑l = l₀
⊢ 0 = ∑' (i : ℕ), 0

case neg
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
l : ↥L.lattice
h : ¬↑l = l₀
⊢ 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2 =
    ∑' (i : ℕ), ((↑i + 1) * (↑l - x) ^ (-↑(i + 2)) - Nat.casesOn i (↑l ^ (-2)) 0) * (z - x) ^ i
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : P.leadingCoeff = 2 ^ (n - 1)
hPdeg' : P.degree = ↑n
⊢ P.coeff n = 2 ^ (n - 1)

Tactic:
rwa [leadingCoeff, natDegree_eq_of_degree_eq_some hPdeg'] at hP

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

Goal state before:
pp: case a
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ z.re ^ 2 / z.im ^ 2 ≤
    { coe := { re := A, im := B }, coe_im_pos := h }.re ^ 2 / { coe := { re := A, im := B }, coe_im_pos := h }.im ^ 2

Tactic:
← even_two.pow_abs

Goal state after:
case a
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ |z.re| ^ 2 / z.im ^ 2 ≤
    { coe := { re := A, im := B }, coe_im_pos := h }.re ^ 2 / { coe := { re := A, im := B }, coe_im_pos := h }.im ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n k : ℕ
hk : k < n
⊢ rootMultiplicity (cos ((↑k + 1) * π / (↑n + 1))) (U ℝ ↑n) = 1

Tactic:
rw [← count_roots, roots_U_real, Multiset.count_eq_one_of_mem (by simp)]

Goal state after:
n k : ℕ
hk : k < n
⊢ cos ((↑k + 1) * π / (↑n + 1)) ∈ (Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)).val
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ MinFacHelper n 3

Tactic:
refine ⟨by simp, by simp, ?_⟩
  refine (le_minFac'.mpr fun p hp hpn ↦ ?_).resolve_left (Nat.ne_of_gt (Nat.le_of_ble_eq_true h1))
  rcases hp.eq_or_lt with rfl | h
  · simp [(Nat.dvd_iff_mod_eq_zero ..).1 hpn] at h2
  · exact h

Goal state after:
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
⊢ MinFacHelper n k'

Tactic:
rw [← e]

Goal state after:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
⊢ MinFacHelper n (k + 2)
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case hbc
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ ∑ i ∈ range N with j < c ^ i, 1 / (c ^ i) ^ 2 ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2

Tactic:
exact sum_div_pow_sq_le_div_sq N hj hc

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
I : Type v
inst✝³ : SmallCategory I
inst✝² : IsFiltered I
J : Type
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ I ⥤ C
hF : ∀ (i : I), IsIndObject (limit (F.flip.obj i ⋙ yoneda))
⊢ IsIndObject (limit (F ⋙ (Functor.whiskeringRight I C (Cᵒᵖ ⥤ Type v)).obj yoneda ⋙ colim))

Tactic:
let G : J ⥤ I ⥤ (Cᵒᵖ ⥤ Type v) := F ⋙ (Functor.whiskeringRight _ _ _).obj yoneda

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type v
inst✝³ : SmallCategory I
inst✝² : IsFiltered I
J : Type
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ I ⥤ C
hF : ∀ (i : I), IsIndObject (limit (F.flip.obj i ⋙ yoneda))
G : J ⥤ I ⥤ Cᵒᵖ ⥤ Type v := F ⋙ (Functor.whiskeringRight I C (Cᵒᵖ ⥤ Type v)).obj yoneda
⊢ IsIndObject (limit (F ⋙ (Functor.whiskeringRight I C (Cᵒᵖ ⥤ Type v)).obj yoneda ⋙ colim))
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 b : ↥S
hb : 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:
hb₁

Goal state after:
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 b : ↥S
hb : b ∈ S.attach
hb₁ : b ≠ v
⊢ Sigma.ι (fun x ↦ f (↑x).as) v ≫ Sigma.π (fun a ↦ f (↑a).as) b ≫ Sigma.ι f (↑b).as = 0
Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset

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

Tactic:
hb₁

Goal state after:
case h₀
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteProducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasProduct f
S : (Finset (Discrete α))ᵒᵖ
v b : ↥(Opposite.unop S)
hb : b ∈ (Opposite.unop S).attach
hb₁ : b ≠ v
⊢ Pi.π f (↑b).as ≫ Pi.ι (fun a ↦ f (↑a).as) b ≫ Pi.π (fun x ↦ f (↑x).as) v = 0
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: case refine_1
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
y y' : (fun X ↦ X) (colimit (pointwiseProduct F))
hy : (hom (colimitPointwiseProductToProductColimit F)) y = (hom (colimitPointwiseProductToProductColimit F)) y'
⊢ y = y'

Tactic:
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)

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
inst✝³ : HasProductsOfShape ι C
inst✝² : IsIPCOfShape.{w, u_1, v, u} ι C
inst✝¹ : HasFilteredColimitsOfSize.{w, w, v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
J : ι → Type w
x✝¹ : (i : ι) → SmallCategory (J i)
x✝ : ∀ (i : ι), IsFiltered (J i)
F : (i : ι) → J i ⥤ D ⥤ C
c : (i : ι) → Cocone (F i)
hc : (i : ι) → IsColimit (c i)
X : D
⊢ IsColimit (((evaluation D C).obj X).mapCocone (coconePointwiseProduct c))

Tactic:
exact IsColimit.equivOfNatIsoOfIso (pointwiseProductCompEvaluation F X).symm _ _
      (evaluationCoconePointwiseProductIso F X c).symm
      (IsIPCOfShape.nonempty_isColimit fun i ↦ isColimitOfPreserves _ (hc i)).some

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
⊢ (Over.Hom.left (Φ.toColon Ψ).hom).app X ≫ (Φ.colon Ψ).ι.app X = Φ.ι.app X

Tactic:
by
  rw [← NatTrans.comp_app, Over.w]

Goal state after:
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 g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ R.extMk f m hm hf - R.extMk g m hm hg = R.extMk (f - g) m hm ⋯

Tactic:
dsimp [extMk]

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 g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) -
      R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (g ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk (Cocycle.fromSingleMk ((f - g) ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))