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

Goal state before:
pp: p : ℝ
⊢ binEntropy p = 0 ↔ p = 0 ∨ p = 1

Tactic:
refine ⟨fun h ↦ ?_, by rintro (rfl | rfl) <;> simp⟩

Goal state after:
p : ℝ
h : binEntropy p = 0
⊢ p = 0 ∨ p = 1
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
p1le2 : p1 < p2
p : ℝ
this : 2 ≤ ↑q
qinv_lt_1 : (↑q)⁻¹ < 1
zero_lt_1_sub_p : 0 < 1 - p
hp : 1 - (↑q)⁻¹ < p ∧ p < 1
qpos : 0 < ↑q
⊢ ↑q - 1 < p * ↑q

Tactic:
have h1 := mul_lt_mul_of_pos_right hp.1 qpos

Goal state after:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
p1le2 : p1 < p2
p : ℝ
this : 2 ≤ ↑q
qinv_lt_1 : (↑q)⁻¹ < 1
zero_lt_1_sub_p : 0 < 1 - p
hp : 1 - (↑q)⁻¹ < p ∧ p < 1
qpos : 0 < ↑q
h1 : (1 - (↑q)⁻¹) * ↑q < p * ↑q
⊢ ↑q - 1 < p * ↑q
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
i : ℕ
hi : i ∈ p.support
ik : i ≤ k
⊢ ↑(p.coeff i) * (↑(b ^ (k - i) * b ^ i / b ^ i) * ↑(a ^ i)) = ↑(p.coeff i) * ↑(a ^ i) * ↑b ^ (k - i)

pp: case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
i : ℕ
hi : i ∈ p.support
ik : i ≤ k
⊢ b ^ i ∣ b ^ (k - i) * b ^ i

Tactic:
Int.mul_ediv_cancel _ (pow_ne_zero _ hb),

Goal state after:
case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
i : ℕ
hi : i ∈ p.support
ik : i ≤ k
⊢ ↑(p.coeff i) * (↑(b ^ (k - i)) * ↑(a ^ i)) = ↑(p.coeff i) * ↑(a ^ i) * ↑b ^ (k - i)

case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
i : ℕ
hi : i ∈ p.support
ik : i ≤ k
⊢ b ^ i ∣ b ^ (k - i) * b ^ i
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: case inr
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : 0 < q
⊢ Monotone fun a ↦ a ^ ↑q

Tactic:
· simp_rw [← CFC.nnrpow_eq_rpow hq]
    exact monotone_nnrpow hp

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
F : Filter ℝ
hpos : ∀ᶠ (t : ℝ) in F, 0 < t
V : E
huni : ∀ δ > 0, ∀ᶠ (t : ℝ) in F, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ
δ : ℝ
hδ : δ > 0
C : ℝ := |log (b / a)|
hC_def : C = |log (b / a)|
δ' : ℝ := δ / (C + 1)
t : ℝ
ht_pos : 0 < t
hbound : ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ'
hlog_eq : log (b * t / (a * t)) = log (b / a)
⊢ ‖(∫ (x : ℝ) in a * t..b * t, x⁻¹ • f x) - log (b / a) • V‖ =
    ‖(∫ (x : ℝ) in a * t..b * t, x⁻¹ • f x) - log (b * t / (a * t)) • V‖

Tactic:
hlog_eq

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
F : Filter ℝ
hpos : ∀ᶠ (t : ℝ) in F, 0 < t
V : E
huni : ∀ δ > 0, ∀ᶠ (t : ℝ) in F, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ
δ : ℝ
hδ : δ > 0
C : ℝ := |log (b / a)|
hC_def : C = |log (b / a)|
δ' : ℝ := δ / (C + 1)
t : ℝ
ht_pos : 0 < t
hbound : ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ'
hlog_eq : log (b * t / (a * t)) = log (b / a)
⊢ ‖(∫ (x : ℝ) in a * t..b * t, x⁻¹ • f x) - log (b / a) • V‖ =
    ‖(∫ (x : ℝ) in a * t..b * t, x⁻¹ • f x) - log (b / a) • V‖
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
F : Filter ℝ
hpos : ∀ᶠ (t : ℝ) in F, 0 < t
V : E
huni : ∀ δ > 0, ∀ᶠ (t : ℝ) in F, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ
δ : ℝ
hδ : δ > 0
C : ℝ := |log (b / a)|
hC_def : C = |log (b / a)|
δ' : ℝ := δ / (C + 1)
t : ℝ
ht_pos : 0 < t
hbound : ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ'
hlog_eq : log (b * t / (a * t)) = log (b / a)
⊢ δ' * |log (b * t / (a * t))| = δ' * C

Tactic:
hlog_eq

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
F : Filter ℝ
hpos : ∀ᶠ (t : ℝ) in F, 0 < t
V : E
huni : ∀ δ > 0, ∀ᶠ (t : ℝ) in F, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ
δ : ℝ
hδ : δ > 0
C : ℝ := |log (b / a)|
hC_def : C = |log (b / a)|
δ' : ℝ := δ / (C + 1)
t : ℝ
ht_pos : 0 < t
hbound : ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ'
hlog_eq : log (b * t / (a * t)) = log (b / a)
⊢ δ' * |log (b / a)| = δ' * C
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: ⊢ Tendsto (fun z ↦ z / 2) (𝓝[≠] 0) (𝓝[≠] 0)

Tactic:
rw [tendsto_nhdsWithin_iff, (by simp : 𝓝 (0 : ℂ) = 𝓝 (0 / 2))]

Goal state after:
⊢ Tendsto (fun z ↦ z / 2) (𝓝[≠] 0) (𝓝 (0 / 2)) ∧ ∀ᶠ (n : ℂ) in 𝓝[≠] 0, n / 2 ∈ {0}ᶜ
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
hint : IntegrableOn (fun x ↦ x⁻¹ • (f (a * x) - f (b * x))) (Ioi 0) volume
⊢ ∫ (x : ℝ) in Ioi 0, x⁻¹ • (f (a * x) - f (b * x)) = log (b / a) • (L - R)

Tactic:
have h_lim := (tendsto_intervalIntegral hf ha hb hL hR).mono_left curry_le_prod
  set g := fun x ↦ x⁻¹ • (f (a * x) - f (b * x)) with hg
  apply tendsto_nhds_unique
    (hint.continuousWithinAt_Ici_primitive_Ioi.mono_left (nhdsWithin_mono 0 Ioi_subset_Ici_self))
  rw [tendsto_nhdsWithin_nhds]
  intro ε hε
  rw [Metric.tendsto_nhds] at h_lim
  specialize h_lim (ε / 2) (by positivity)
  rw [eventually_curry_iff, Filter.Eventually, mem_nhdsWithin_iff] at h_lim
  obtain ⟨δ, hδ_pos, hδ⟩ := h_lim
  simp_rw [subset_def, mem_inter_iff, mem_ball] at hδ
  refine ⟨δ, hδ_pos, ?_⟩
  intro x hx hdist
  specialize hδ x ⟨hdist, hx⟩
  rw [mem_ofPred] at hδ
  have hint' : IntegrableOn g (Ioi x) := hint.mono (by grind) (by simp)
  have htends := intervalIntegral_tendsto_integral_Ioi x hint' tendsto_id
  have hle := le_of_tendsto (htends.dist tendsto_const_nhds) (hδ.mono (fun _ hy ↦ hy.le))
  linarith

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

Tactic:
← rpow_lt_rpow_iff (z := 60),

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 ^ (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: case hb
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ (fun s ↦ 2 ^ (1 - 2 * s)) (1 / 2)

Tactic:
exact (differentiableAt_const _).rpow (by fun_prop) two_ne_zero

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
h2 : 0 < (↑π / a).re
f_bd : f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
x : ℝ
⊢ -(↑π * a⁻¹ * ↑x * I * b * 2) - ↑π * a⁻¹ * ↑x ^ 2 - ↑π * a⁻¹ * I ^ 2 * b ^ 2 =
    -(↑π * a⁻¹ * ↑x * I * b * 2) - ↑π * a⁻¹ * ↑x ^ 2 + ↑π * a⁻¹ * b ^ 2

Tactic:
I_sq

Goal state after:
a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
h2 : 0 < (↑π / a).re
f_bd : f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
x : ℝ
⊢ -(↑π * a⁻¹ * ↑x * I * b * 2) - ↑π * a⁻¹ * ↑x ^ 2 - ↑π * a⁻¹ * -1 * b ^ 2 =
    -(↑π * a⁻¹ * ↑x * I * b * 2) - ↑π * a⁻¹ * ↑x ^ 2 + ↑π * a⁻¹ * b ^ 2
Module: Mathlib.Data.Int.Log

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
⊢ Nat.log b ⌊r⁻¹⌋₊ = 0

Tactic:
Nat.log_eq_zero_iff

Goal state after:
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case h.right
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ logb b (b ^ x) = x

Tactic:
logb_rpow b_pos b_ne_one

Goal state after:
case h.right
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ x = x
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
⊢ ConcaveOn ℝ (Ici 0) (cfc (p.rpowIntegrand₀₁ t))

Tactic:
have h₁ : (Ici (0 : A)).EqOn (cfc (rpowIntegrand₀₁ p t))
      (fun x : A =>
        algebraMap ℝ A (t ^ (p - 1)) - t ^ p • Ring.inverse (algebraMap ℝ A t + x)) := by
    intro x hx
    rw [rpowIntegrand₀₁_eq_sub (by grind) ht]
    have hg : ContinuousOn (fun z : ℝ => (t + z)⁻¹) (spectrum ℝ x) := by
      fun_prop (disch := grind -abstractProof)
    have hf : ContinuousOn (fun z : ℝ => (1 + z)) (spectrum ℝ x) := by fun_prop
    have hspectrum :  ∀ r ∈ spectrum ℝ x, t + r ≠ 0 := by grind
    have := cfc_sub (fun _ : ℝ => t ^ (p - 1)) (fun z : ℝ => t ^ p * (t + z)⁻¹) x
    rw [this, cfc_const .., cfc_const_mul .., cfc_inv _ _ hspectrum .., cfc_const_add ..,
        cfc_id' ..]
  refine ConcaveOn.congr ?_ h₁.symm
  refine ConcaveOn.sub (concaveOn_const _ (convex_Ici 0)) ?_
  exact ConvexOn.smul (by positivity) <| CStarAlgebra.convexOn_ringInverse_algebraMap_add ht

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
⊢ LipschitzWith 1 ε.mulExpNegMulSq

Tactic:
apply lipschitzWith_of_nnnorm_deriv_le differentiable_mulExpNegMulSq

Goal state after:
ε : ℝ
hε : 0 < ε
⊢ ∀ (x : ℝ), ‖deriv ε.mulExpNegMulSq x‖₊ ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Pochhammer

Goal state before:
pp: n : ℕ
hn : n ≠ 0
ι : Type u_2
t : Finset ι
p : ι → ℕ
w : ι → ℝ
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : ∑ i ∈ t, w i = 1
h_avg : ↑n - 1 ≤ ∑ i ∈ t, w i * ↑(p i)
⊢ Polynomial.eval (∑ i ∈ t, w i * ↑(p i)) (descPochhammer ℝ n) / ↑n.factorial ≤
    ∑ x ∈ t, w x * (Polynomial.eval (↑(p x)) (descPochhammer ℝ n) / ↑n.factorial)

Tactic:
mul_div,

Goal state after:
n : ℕ
hn : n ≠ 0
ι : Type u_2
t : Finset ι
p : ι → ℕ
w : ι → ℝ
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : ∑ i ∈ t, w i = 1
h_avg : ↑n - 1 ≤ ∑ i ∈ t, w i * ↑(p i)
⊢ Polynomial.eval (∑ i ∈ t, w i * ↑(p i)) (descPochhammer ℝ n) / ↑n.factorial ≤
    ∑ x ∈ t, w x * Polynomial.eval (↑(p x)) (descPochhammer ℝ n) / ↑n.factorial
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
g : ℝ → ℝ := fun t ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
t : ℝ
⊢ t ∈ Ioi 0 → 0 ≤ g t

Tactic:
t_pos

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
t : ℝ
t_pos : t ∈ Ioi 0
⊢ 0 ≤ g t
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

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

pp: case hf
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable fun l ↦ if ↑l = ↑l₀ then 0 else 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2

pp: case hg
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable fun i ↦ if ↑i = ↑l₀ then 1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2 else 0

Tactic:
· congr with w; split_ifs <;> simp only [zero_add, add_zero, *]

Goal state after:
case hf
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable fun l ↦ if ↑l = ↑l₀ then 0 else 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2

case hg
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable fun i ↦ if ↑i = ↑l₀ then 1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2 else 0
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: case neg.hc'
a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
⊢ Tendsto (fun n ↦ ‖regularizedHGFunCoeff a b n.succ‖ / ‖regularizedHGFunCoeff a b n‖) atTop (𝓝 0)

Tactic:
simp only [Nat.succ_eq_add_one]
    have h₁ : Tendsto (fun (n : ℕ) ↦ (n : ℂ) ^ (a.card - (b.card : ℤ) - 1)) atTop (𝓝 0) := by
      have := (tendsto_one_div_atTop_nhds_zero_nat (𝕜 := ℂ)).pow (b.card + 1 - a.card)
      rw [zero_pow (by grind)] at this
      apply this.congr
      intro n
      rw [one_div, inv_pow, ← zpow_natCast, ← zpow_neg, Int.ofNat_sub (by grind),
        Int.natCast_add_one]
      ring_nf
    have := (h₁.mul (tendsto_multiset_prod_div_multiset_prod_mul a b)).norm
    simp only [mul_one, norm_zero] at this
    apply this.congr'
    have h_ne := eventually_atTop_regularizedHGFunCoeff_ne_zero b ha
    filter_upwards [h_ne, Filter.eventually_ne_atTop 0] with n hn₁ hn₂
    rw [← Complex.norm_div, regularizedHGFunCoeff_add_one_div_self hn₁,
      multiset_prod_div_multiset_prod_mul a b hn₂, mul_div]

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

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

Tactic:
← (Equiv.addRight l).tsum_eq

Goal state after:
L : PeriodPair
l₀ z : ℂ
l : ↥L.lattice
⊢ (∑' (c : ↥L.lattice), if ↑((Equiv.addRight l) c) = l₀ then 0 else -2 / (z + ↑l - ↑((Equiv.addRight l) c)) ^ 3) =
    ∑' (l_1 : ↥L.lattice), if ↑l_1 = l₀ - ↑l then 0 else -2 / (z - ↑l_1) ^ 3
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ ℘[L] (z - ↑l) = ℘[L] z

Tactic:
rw [← L.weierstrassP_add_coe _ l, sub_add_cancel]

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

Goal state before:
pp: L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ -∑' (l_1 : ↥L.lattice), 2 / (z + ↑l - ↑l_1) ^ 3 = -∑' (l : ↥L.lattice), 2 / (z - ↑l) ^ 3

Tactic:
← (Equiv.addRight l).tsum_eq

Goal state after:
L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ -∑' (c : ↥L.lattice), 2 / (z + ↑l - ↑((Equiv.addRight l) c)) ^ 3 = -∑' (l : ↥L.lattice), 2 / (z - ↑l) ^ 3
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ IsIntegral ℤ (2 * cos (↑q * ↑π))

Tactic:
rw [cos.eq_1, mul_div_cancel₀ _ two_ne_zero]
  exact (isIntegral_exp_rat_mul_pi_mul_I q).add (isIntegral_exp_neg_rat_mul_pi_mul_I q)

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

Goal state before:
pp: n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
⊢ (-1) ^ (-k) = (-1) ^ k

Tactic:
← Int.cast_negOnePow,

Goal state after:
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
⊢ ↑↑(-k).negOnePow = (-1) ^ k
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
⊢ P = T ℝ ↑n → sumNodes n c P = sumNodes n c (T ℝ ↑n)

Tactic:
intro h; rw [h]

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

Goal state before:
pp: n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
s : Finset ℕ
hs : s ⊆ (Finset.range (n + 1)).erase i
hscard : s.card = n - k
hsn : 0 ∉ s
a : ℕ
ha : a ∈ s
⊢ node n a < 1

Tactic:
← node_eq_one (n := n)

Goal state after:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
s : Finset ℕ
hs : s ⊆ (Finset.range (n + 1)).erase i
hscard : s.card = n - k
hsn : 0 ∉ s
a : ℕ
ha : a ∈ s
⊢ node n a < node n 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
s : Finset ℕ
hs : s ⊆ (Finset.range (n + 1)).erase i
hscard : s.card = n - k
hsn : 0 ∉ s
a : ℕ
ha : a ∈ s
⊢ node n a < 1

Tactic:
rw [← node_eq_one (n := n)]

Goal state after:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
s : Finset ℕ
hs : s ⊆ (Finset.range (n + 1)).erase i
hscard : s.card = n - k
hsn : 0 ∉ s
a : ℕ
ha : a ∈ s
⊢ node n a < node n 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
x : ℂ
this : Differentiable ℂ L.relation
z w : ℂ
hw : w ∈ L.lattice
⊢ L.relation (z + w) = L.relation z

Tactic:
lift w to L.lattice using hw

Goal state after:
L : PeriodPair
x : ℂ
this : Differentiable ℂ L.relation
z : ℂ
w : ↥L.lattice
⊢ L.relation (z + ↑w) = L.relation z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

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

Tactic:
by
  rw [Complex.cot, Complex.sin, Complex.cos]
  have h1 : exp (z * I) + exp (-z * I) = exp (-(z * I)) * (exp (2 * I * z) + 1) := by
    rw [mul_add, ← Complex.exp_add]
    ring_nf
  have h2 : (exp (-z * I) - exp (z * I)) = exp (-(z * I)) * ((1 - exp (2 * I * z))) := by
    ring_nf
    rw [mul_assoc, ← Complex.exp_add]
    ring_nf
  rw [h1, h2]
  field

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

Goal state before:
pp: z : ℂ
⊢ (↑π * z).cot = (cexp (2 * ↑π * I * z) + 1) / (I * (1 - cexp (2 * ↑π * I * z)))

Tactic:
rw [cot_eq_exp_ratio (π * z)]

Goal state after:
z : ℂ
⊢ (cexp (2 * I * (↑π * z)) + 1) / (I * (1 - cexp (2 * I * (↑π * z)))) =
    (cexp (2 * ↑π * I * z) + 1) / (I * (1 - cexp (2 * ↑π * I * z)))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
x : ℝ
hroot : x ∈ Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((2 * ↑k + 1) * π / (2 * ↑n)) = x
hn : n ≠ 0
hnz : (Rat.divInt (2 * ↑k + 1) (2 * ↑n)).den ≤ 3
⊢ (Rat.divInt (2 * ↑k + 1) (2 * ↑n)).den = 2 * n / (2 * n).gcd (2 * k + 1)

Tactic:
rw [Rat.den_divInt]

Goal state after:
n : ℕ
x : ℝ
hroot : x ∈ Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((2 * ↑k + 1) * π / (2 * ↑n)) = x
hn : n ≠ 0
hnz : (Rat.divInt (2 * ↑k + 1) (2 * ↑n)).den ≤ 3
⊢ (if 2 * ↑n = 0 then 1 else (2 * ↑n).natAbs / (2 * ↑n).gcd (2 * ↑k + 1)) = 2 * n / (2 * n).gcd (2 * k + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

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

Tactic:
filter_upwards with n z hz using hu2 n z hz

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: β : Type u_2
inst✝ : CommRing β
⊢ (monomial { order := 2, coeffs := ![1, 1] }.order) 1 -
      ∑ i, (monomial ↑i) ({ order := 2, coeffs := ![1, 1] }.coeffs i) =
    X ^ 2 - (X + 1)

Tactic:
simp [Finset.sum_fin_eq_sum_range, Finset.sum_range_succ', ← smul_X_eq_monomial]

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

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

Tactic:
mul_div,

Goal state after:
n : ℕ
⊢ (φ ^ (n + 1) - ψ ^ (n + 1)) / √5 - φ * (φ ^ n - ψ ^ n) / √5 = ψ ^ n
Module: Mathlib.Analysis.SumIntegralComparisons

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

Tactic:
by
    gcongr with i hi
    rw [Finset.mem_range, ← Nat.add_one_le_iff] at hi
    have := hf.intervalIntegrable_subset _ hi
    rify at hi this ⊢
    refine integral_mono_on (by simp) this (by simp) fun _ _ ↦ by apply hf <;> grind

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.inl ≫
      biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) ≫ biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)) =
    biprod.inl ≫ 0

Tactic:
biprod.inl_desc_assoc,

Goal state after:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ biprod.inl) ≫ biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)) = biprod.inl ≫ 0
Module: Mathlib.CategoryTheory.Generator.Preadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ IsCoseparator G ↔ (preadditiveYonedaObj G).Faithful

Tactic:
by
  rw [isCoseparator_iff_faithful_preadditiveYoneda, preadditiveYoneda_obj]
  exact ⟨fun h => Functor.Faithful.of_comp _ (forget₂ _ AddCommGrpCat.{v}),
    fun h => Functor.Faithful.comp _ _⟩

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

Goal state before:
pp: case refine_2
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ Tendsto (HPow.hPow (c k)) atTop atTop

Tactic:
exact tendsto_pow_atTop_atTop_of_one_lt (cone k)

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
M : ℕ
hM : 0 < M
⊢ ∫ (x : ℝ) in ↑N..↑M + ↑N, ‖f x‖ ≤ ∑' (n : ℕ), f ↑(n + N)

Tactic:
calc
      _ = ∫ x in N..M+N, f x := by
        refine intervalIntegral.integral_congr_uIoo fun x ↦ ?_
        grind [Real.norm_of_nonneg, uIoo_of_le]
      _ ≤ ∑ n ∈ Finset.range M, f (n + N : ℕ) := by
        convert! AntitoneOn.integral_le_sum (anti.mono _) using 2 <;> grind
      _ ≤ _ := by grind [summable.sum_le_tsum, Nat.cast_pos]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
h : PreservesFiniteLimits A
⊢ IsFiltered (CostructuredArrow yoneda A)

Tactic:
exact isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits A

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

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ Cᵒᵖ ⥤ Type v
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} ↑(s i)
j : (i : I) → CostructuredArrow yoneda (F.obj i) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
i : I
y : (F.obj i).obj (Opposite.op A.left)
hy : yonedaEquiv A.hom = (ConcreteCategory.hom ((colimit.ι F i).app (Opposite.op A.left))) y
y' : CostructuredArrow yoneda (F.obj i) := CostructuredArrow.mk (yonedaEquiv.symm y)
x : y' ⟶ j i y'
⊢ yonedaEquiv (yoneda.map (𝟙 A.left) ≫ ((CostructuredArrow.map (colimit.ι F i)).obj y').hom) = yonedaEquiv A.hom

Tactic:
simp [-EmbeddingLike.apply_eq_iff_eq, hy, yonedaEquiv_comp, y']

Goal state after: