mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: A : Type u_2
inst✝ : NormedRing A
v : A →+* ℂ
hv : Isometry ⇑v
n : ℕ
p : A[X]
⊢ ‖p.coeff n‖ ≤ ↑(p.natDegree.choose n) * p.mapMahlerMeasure v

Tactic:
by
  have hv_norm : ‖p.coeff n‖ = ‖v (p.coeff n)‖ :=
    (hv.norm_map_of_map_zero (map_zero _) _).symm
  have hcoeff : ‖v (p.coeff n)‖ = ‖(p.map v).coeff n‖ := by simp
  grw [hv_norm, hcoeff, norm_coeff_le_choose_mul_mahlerMeasure,
    natDegree_map_eq_of_injective hv.injective, mapMahlerMeasure]

Goal state after:
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
⊢ x.InfinitePos ↔ 0 < x ∧ ArchimedeanClass.mk x < 0

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨hx, hx'⟩ r ↦ ?_⟩
  · have hx : 0 < x := h 0
    refine ⟨h 0, fun n ↦ ?_⟩
    simpa [abs_of_pos hx] using! h n
  · exact lt_of_mk_lt_mk_of_nonneg (hx'.trans_le <| mk_map_nonneg_of_archimedean coeRingHom _) hx.le

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

Goal state before:
pp: x : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational (x * ↑q * ↑q⁻¹)

Tactic:
rwa [mul_assoc, ← cast_mul, mul_inv_cancel₀ hq, cast_one, mul_one]

Goal state after:
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
hni : 0 ≤ ArchimedeanClass.mk x
⊢ x.IsSt (sSup {y | ↑y < x})

Tactic:
isSt_iff

Goal state after:
x : ℝ*
hni : 0 ≤ ArchimedeanClass.mk x
⊢ 0 ≤ ArchimedeanClass.mk x ∧ stdPart x = sSup {y | ↑y < x}
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x y : ℝ*
⊢ x.InfiniteNeg → ¬y.InfinitePos → (x + y).InfiniteNeg

Tactic:
rw [← infinitePos_neg, ← infinitePos_neg, ← @infiniteNeg_neg y, neg_add]

Goal state after:
x y : ℝ*
⊢ (-x).InfinitePos → ¬(-y).InfiniteNeg → (-x + -y).InfinitePos
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ rexp (arcosh x) = rexp 0 ↔ x = 1

Tactic:
exp_arcosh hx,

Goal state after:
x : ℝ
hx : 1 ≤ x
⊢ x + √(x ^ 2 - 1) = rexp 0 ↔ x = 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case hx₁
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -π < 2 * z.re

Tactic:
rwa [← div_lt_iff₀' two_pos, neg_div]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
⊢ 0 < re 1 + z.re ∨ 1 + z = 0

Tactic:
one_re,

Goal state after:
z : ℂ
hz : ‖z‖ < 1
⊢ 0 < 1 + z.re ∨ 1 + z = 0
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: case inl
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : |z.im| ≤ z.re
⊢ ↑n * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖

Tactic:
rwa [max_eq_left hle]

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

Goal state before:
pp: l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ z : ℂ
hz : z ≠ 0
⊢ (fun z ↦ z ^ a₁ * cexp (↑b₁ * z)) z = (fun z ↦ z ^ a₂ * cexp (↑b₁ * z) * z ^ (a₁ - a₂)) z

Tactic:
by
        simp only
        rw [mul_right_comm, ← cpow_add _ _ hz, add_sub_cancel]

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: n : ℕ
⊢ ((2 * (2 * ↑n + 3)) • sinPoly (n + 1) + (monomial 2) (-4) * sinPoly n).natDegree ≤ n + 2

Tactic:
refine natDegree_add_le_of_degree_le ((natDegree_smul_le _ _).trans ?_) ?_

Goal state after:
case refine_1
n : ℕ
⊢ (sinPoly (n + 1)).natDegree ≤ n + 2

case refine_2
n : ℕ
⊢ ((monomial 2) (-4) * sinPoly n).natDegree ≤ n + 2
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: n : ℕ
⊢ ((2 * (2 * ↑n + 3)) • cosPoly (n + 1) + (monomial 2) (-4) * cosPoly n).natDegree ≤ n + 2

Tactic:
refine natDegree_add_le_of_degree_le ((natDegree_smul_le _ _).trans ?_) ?_

Goal state after:
case refine_1
n : ℕ
⊢ (cosPoly (n + 1)).natDegree ≤ n + 2

case refine_2
n : ℕ
⊢ ((monomial 2) (-4) * cosPoly n).natDegree ≤ n + 2
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: ⊢ StrictMonoOn binEntropy (Icc 0 2⁻¹)

Tactic:
rw [show Icc (0 : ℝ) 2⁻¹ = Icc 0 (1 - 1 / 2) by norm_num, ← qaryEntropy_two]
  exact qaryEntropy_strictMonoOn (by rfl)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a ≤ b
⊢ a ^ (1 / 2) ≤ b ^ (1 / 2)

Tactic:
refine (monotone_nnrpow (A := A) ?_) hab

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a ≤ b
⊢ 1 / 2 ∈ Icc 0 1
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) * (↑a ^ i / ↑b ^ i) * ↑b ^ k = ↑(p.coeff i) * ↑a ^ i * ↑b ^ (k - i)

Tactic:
rw [mul_assoc, div_mul_comm, ← Int.cast_pow, ← Int.cast_pow, ← Int.cast_pow,
    ← pow_sub_mul_pow b ik, ← Int.cast_div_charZero, Int.mul_ediv_cancel _ (pow_ne_zero _ hb),
    ← mul_assoc, mul_right_comm, ← Int.cast_pow]

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
⊢ b ^ i ∣ b ^ (k - i) * b ^ i
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order

Goal state before:
pp: case pos
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
⊢ Tendsto (fun i ↦ if a ∈ {b | IsStrictlyPositive b} then cfc (fun x ↦ i⁻¹ * (x ^ i - 1)) a else 0) (𝓝[>] 0)
    (𝓝 (if a ∈ {b | IsStrictlyPositive b} then log a else 0))

Tactic:
simpa [ha] using CFC.tendsto_cfc_rpow_sub_one_log ha

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: case h.refine_1
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
r : ℝ
hr : r ∈ spectrum ℝ z
this✝ : 0 < r
this : 0 ≤ b * r
⊢ a + b * r ≠ 0 ∨ 0 ≤ -1

Tactic:
cases lt_or_eq_of_le ha

Goal state after:
case h.refine_1.inl
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
r : ℝ
hr : r ∈ spectrum ℝ z
this✝ : 0 < r
this : 0 ≤ b * r
h✝ : 0 < a
⊢ a + b * r ≠ 0 ∨ 0 ≤ -1

case h.refine_1.inr
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
r : ℝ
hr : r ∈ spectrum ℝ z
this✝ : 0 < r
this : 0 ≤ b * r
h✝ : 0 = a
⊢ a + b * r ≠ 0 ∨ 0 ≤ -1
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t : ℝ
ht : 0 < t
⊢ EqOn (p.rpowIntegrand₀₁ t) (fun x ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) (Ici 0)

Tactic:
intro x hx
  calc _ = t ^ p * (t⁻¹ - t⁻¹ * (1 + x * t⁻¹)⁻¹) := by simp [field, rpowIntegrand₀₁]
    _ = t ^ (p - 1) * (1 - (1 + x * t⁻¹)⁻¹) := by
          rw [Real.rpow_sub_one ht.ne']
          ring
    _ = _ := by simp [mul_comm, smul_eq_mul, rpowIntegrand₀₁]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ IntegrableOn (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (Ioi 1) volume

Tactic:
by
  refine ⟨?meas, ?finite⟩
  case meas =>
    refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioi
    exact continuousOn_rpowIntegrand₀₁ hp hx |>.mono (Set.Ioi_subset_Ioi zero_le_one)
  case finite =>
    refine HasFiniteIntegral.mono' (g := fun t => t ^ (p - 2) * x) ?finitebound ?ae_le
    case finitebound =>
      refine HasFiniteIntegral.mul_const ?_ _
      apply Integrable.hasFiniteIntegral
      rw [Set.mem_Ioo] at hp
      refine integrableOn_Ioi_rpow_of_lt ?_ zero_lt_one
      linarith
    case ae_le =>
      refine ae_restrict_of_forall_mem measurableSet_Ioi fun t (ht : 1 < t) => ?_
      rw [Real.norm_of_nonneg (rpowIntegrand₀₁_nonneg hp.1 (by positivity) hx)]
      exact rpowIntegrand₀₁_le_rpow_sub_two_mul_self hp (by positivity) hx

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

Goal state before:
pp: ⊢ HasDerivAt Gammaℂ (-(↑γ + log (2 * ↑π)) / ↑π) 1

Tactic:
by
  let f (s : ℂ) : ℂ := 2 * (2 * π) ^ (-s)
  have : HasDerivAt (fun s : ℂ ↦ 2 * (2 * π : ℂ) ^ (-s)) (-log (2 * π) / π) 1 := by
    have := (hasDerivAt_neg' (1 : ℂ)).const_cpow (c := 2 * π)
      (Or.inl (by exact_mod_cast Real.two_pi_pos.ne'))
    refine (this.const_mul 2).congr_deriv ?_
    rw [mul_neg_one, mul_neg, cpow_neg_one, ← div_eq_inv_mul, ← mul_div_assoc,
      mul_div_mul_left _ _ two_ne_zero, neg_div]
  have := this.mul hasDerivAt_Gamma_one
  rwa [Gamma_one, mul_one, cpow_neg_one, ← div_eq_mul_inv, ← div_div, div_self two_ne_zero,
    mul_comm (1 / _), mul_one_div, ← _root_.add_div, ← neg_add, add_comm] at this

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case succ
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b n✝ : ℕ
⊢ log b ↑(n✝ + 1) = ↑(Nat.log b (n✝ + 1))

Tactic:
rw [log_of_one_le_right, Nat.floor_natCast]

Goal state after:
case succ.hr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b n✝ : ℕ
⊢ 1 ≤ ↑(n✝ + 1)
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: x : ℝ
⊢ mulExpNegMulSq 1 x ≤ 1

Tactic:
by
  simp only [mulExpNegMulSq, one_mul]
  rw [← le_div_iff₀ (exp_pos (-(x * x))), exp_neg, div_inv_eq_mul, one_mul]
  apply le_trans _ (add_one_le_exp (x * x))
  nlinarith

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 μ
f : X →ᵇ ℝ≥0
x : X
key : f x ≤ nndist f 0
⊢ ↑(f x) ≤ ↑(nndist f 0)

Tactic:
rwa [ENNReal.coe_le_coe]

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

Goal state before:
pp: case inl
n : ℕ
h_eq : n = 0
⊢ ConvexOn ℝ (Set.Ici (↑n - 1)) fun x ↦ Polynomial.eval x (descPochhammer ℝ n)

pp: case inr
n : ℕ
h✝ : n > 0
⊢ ConvexOn ℝ (Set.Ici (↑n - 1)) fun x ↦ Polynomial.eval x (descPochhammer ℝ n)

Tactic:
· simp [h_eq, convexOn_const, convex_Ici]

Goal state after:
case inr
n : ℕ
h✝ : n > 0
⊢ ConvexOn ℝ (Set.Ici (↑n - 1)) fun x ↦ Polynomial.eval x (descPochhammer ℝ n)
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
⊢ MeasurePreserving (⇑(homeomorphUnitSphereProd E)) (comap Subtype.val μ) (μ.toSphere.prod (volumeIoiPow (dim E - 1)))

Tactic:
refine ⟨(homeomorphUnitSphereProd E).measurable, .symm ?_⟩

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
⊢ μ.toSphere.prod (volumeIoiPow (dim E - 1)) = map (⇑(homeomorphUnitSphereProd E)) (comap Subtype.val μ)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n a : ℕ
H : ∃ c, a < (c + 1) ^ (n + 1)
c : ℕ
hc : c = Nat.find H
⊢ c ^ (n + 1) ≤ a

Tactic:
cases c with

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

Goal state before:
pp: r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ 4 * ‖s‖ * ‖2 * l - s‖ / ‖l‖ ^ 4 ≤ 4 * r * (2.5 * ‖l‖) / ‖l‖ ^ 4

Tactic:
gcongr (4 * ?_ * ?_) / ‖l‖ ^ 4

Goal state after:
case h₂
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ ‖2 * l - s‖ ≤ 2.5 * ‖l‖
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
x✝¹ : ℝ
x✝ : x✝¹ > 0
⊢ -3 < -↑(finrank ℤ ↥L.lattice)

Tactic:
by simp; norm_num

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

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

Tactic:
refine .fun_sum fun i hi ↦ ?_

Goal state after:
case refine_1
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
⊢ DifferentiableOn ℂ (fun z ↦ if ↑i = l₀ then 0 else 1 / (z - ↑i) ^ 2 - 1 / ↑i ^ 2) (↑L.lattice \ {l₀})ᶜ
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
h₁ : Tendsto (fun n ↦ ↑n ^ (↑a.card - ↑b.card - 1)) atTop (𝓝 0)
this :
  Tendsto
    (fun x ↦
      ‖↑x ^ (↑a.card - ↑b.card - 1) *
          ((Multiset.map (fun x_1 ↦ x_1 / ↑x + 1) a).prod /
            ((Multiset.map (fun x_1 ↦ x_1 / ↑x + 1) b).prod * (1 + (↑x)⁻¹)))‖)
    atTop (𝓝 ‖0 * 1‖)
⊢ Tendsto (fun n ↦ ‖regularizedHGFunCoeff a b (n + 1)‖ / ‖regularizedHGFunCoeff a b n‖) atTop (𝓝 0)

Tactic:
simp only [mul_one, norm_zero] at this

Goal state after:
case neg.hc'
a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
h₁ : Tendsto (fun n ↦ ↑n ^ (↑a.card - ↑b.card - 1)) atTop (𝓝 0)
this :
  Tendsto
    (fun x ↦
      ‖↑x ^ (↑a.card - ↑b.card - 1) *
          ((Multiset.map (fun x_1 ↦ x_1 / ↑x + 1) a).prod /
            ((Multiset.map (fun x_1 ↦ x_1 / ↑x + 1) b).prod * (1 + (↑x)⁻¹)))‖)
    atTop (𝓝 0)
⊢ Tendsto (fun n ↦ ‖regularizedHGFunCoeff a b (n + 1)‖ / ‖regularizedHGFunCoeff a b n‖) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ Set.EqOn (fun x ↦ ℘[L - l₀] (x + ↑l)) (fun x ↦ ℘[L - l₀ - ↑l] x + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2))
    (↑L.lattice \ {l₀ - ↑l})ᶜ

Tactic:
apply IsOpen.eqOn_of_deriv_eq (𝕜 := ℂ) L.isOpen_compl_lattice_sdiff
    ?_ ?_ ?_ ?_ (x := -(l / 2)) ?_ ?_

Goal state after:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ IsPreconnected (↑L.lattice \ {l₀ - ↑l})ᶜ

L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ DifferentiableOn ℂ (fun x ↦ ℘[L - l₀] (x + ↑l)) (↑L.lattice \ {l₀ - ↑l})ᶜ

L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ DifferentiableOn ℂ (fun x ↦ ℘[L - l₀ - ↑l] x + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2)) (↑L.lattice \ {l₀ - ↑l})ᶜ

L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ Set.EqOn (deriv fun x ↦ ℘[L - l₀] (x + ↑l)) (deriv fun x ↦ ℘[L - l₀ - ↑l] x + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2))
    (↑L.lattice \ {l₀ - ↑l})ᶜ

L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ -(↑l / 2) ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ

L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ ℘[L - l₀] (-(↑l / 2) + ↑l) = ℘[L - l₀ - ↑l] (-(↑l / 2)) + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

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

Tactic:
by
  /- We want to write `f b - f a = ∫ x in Icc a b, deriv f x` and use the inequality between
  norm of integral and integral of norm. There is a small difficulty that this formula is not
  true when `E` is not complete, so we need to go first to the completion, and argue there. -/
  let g := UniformSpace.Completion.toComplₗᵢ (𝕜 := ℝ) (E := E)
  have : ‖(g ∘ f) b - (g ∘ f) a‖ₑ = ‖f b - f a‖ₑ := by
    rw [← edist_eq_enorm_sub, Function.comp_def, g.isometry.edist_eq, edist_eq_enorm_sub]
  rw [← this, ← integral_deriv_of_contDiffOn_Icc (g.contDiff.comp_contDiffOn h) hab,
    integral_of_le hab, restrict_Ioc_eq_restrict_Icc]
  apply (enorm_integral_le_lintegral_enorm _).trans
  apply lintegral_mono_ae
  rw [← restrict_Ioo_eq_restrict_Icc]
  filter_upwards [self_mem_ae_restrict measurableSet_Ioo] with x hx
  rw [fderiv_comp_deriv]; rotate_left
  · exact (g.contDiff.differentiable one_ne_zero).differentiableAt
  · exact (h x ⟨hx.1.le, hx.2.le⟩).contDiffAt (Icc_mem_nhds hx.1 hx.2)
      |>.differentiableAt one_ne_zero
  have : fderiv ℝ g (f x) = g.toContinuousLinearMap := g.toContinuousLinearMap.fderiv
  simp [this]

Goal state after:
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.coeff P.natDegree = 2 ^ (n - 1)
hPdeg' : P.degree = ↑n
⊢ P.coeff n = 2 ^ (n - 1)

Tactic:
natDegree_eq_of_degree_eq_some hPdeg'

Goal state after:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : P.coeff n = 2 ^ (n - 1)
hPdeg' : P.degree = ↑n
⊢ P.coeff n = 2 ^ (n - 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℤ
x : ℝ
hx : x ≤ -1
⊢ 1 ≤ ↑↑n.negOnePow * eval x (T ℝ n)

Tactic:
rw [← neg_neg x, T_eval_neg]
  convert! one_le_eval_T_real n (le_neg_of_le_neg hx)
  rw [Int.cast_negOnePow, ← mul_assoc, ← mul_zpow]
  simp

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

Goal state before:
pp: case pos
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hk : n < k
⊢ eval x 0 ≤ eval x ((⇑derivative)^[k] (T ℝ ↑n))

Tactic:
iterate_derivative_eq_zero_of_degree_lt (by simp [hk])

Goal state after:
case pos
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hk : n < k
⊢ eval x 0 ≤ eval x 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
⊢ eval x (T ℝ ↑n) = -1 ↔ ∃ k ≤ n, Odd k ∧ x = cos (↑k * π / ↑n)

Tactic:
constructor
  · intro hx
    obtain ⟨k, hk₁, hk₂⟩ := (abs_eval_T_real_eq_one_iff hn x).mp
      ((abs_eq_abs.mpr (.inl hx)).trans ((abs_neg 1).trans abs_one))
    use k
    refine ⟨hk₁, ?_, hk₂⟩
    rw [hk₂, eval_T_real_cos_int_mul_pi_div hn, Int.cast_negOnePow_natCast] at hx
    exact (neg_one_pow_eq_neg_one_iff_odd (by grind)).mp hx
  · rintro ⟨k, hk₁, hk₂, hx⟩
    rw [hx, eval_T_real_cos_int_mul_pi_div hn, Int.negOnePow_odd k ((Int.odd_coe_nat k).mpr hk₂)]
    norm_cast

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

Goal state before:
pp: z : ℂ
hz : z ≠ 0
c₁ c₂ : ℤ
⊢ (fun n ↦ ((↑n * z + ↑c₁) * (↑n * z + ↑c₂))⁻¹) =O[cofinite] fun n ↦ (|↑n| ^ 2)⁻¹

Tactic:
simp only [Real.rpow_two, abs_mul_abs_self, pow_two]

Goal state after:
z : ℂ
hz : z ≠ 0
c₁ c₂ : ℤ
⊢ (fun n ↦ ((↑n * z + ↑c₁) * (↑n * z + ↑c₂))⁻¹) =O[cofinite] fun n ↦ (↑n * ↑n)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
i : ℕ
⊢ logDeriv (fun z ↦ 1 + sineTerm z i) x = cotTerm x i

Tactic:
have h1 := integerComplement_add_ne_zero hx (i + 1)

Goal state after:
x : ℂ
hx : x ∈ ℂ_ℤ
i : ℕ
h1 : x + ↑(↑i + 1) ≠ 0
⊢ logDeriv (fun z ↦ 1 + sineTerm z i) x = cotTerm x i
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
⊢ Summable fun n ↦ ‖(↑(n + 1) ^ (1 + k))⁻¹‖

Tactic:
summable_norm_iff,

Goal state after:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
⊢ Summable fun n ↦ (↑(n + 1) ^ (1 + k))⁻¹
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ AntitoneOn f (Icc (↑a) (↑a + ↑(b - a)))

Tactic:
by simp [hf, hab]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k : Y ⊞ Z ⟶ A
hk : φ f g ≫ k = 0
⊢ { l // π f g ≫ l = k }

Tactic:
refine ⟨cokernel.desc _ (biprod.inr ≫ k) ?_, ?_⟩
    all_goals
      obtain ⟨k₁, k₂, rfl⟩ := biprod.decomp_hom_from k
      simp only [comp_add, φ_snd_assoc, biprod.ext_from_iff, inl_φ_assoc,
        BinaryBicone.inl_fst_assoc, BinaryBicone.inl_snd_assoc, zero_comp, add_zero, comp_zero,
        inr_φ_fst_assoc, neg_comp, id_comp, BinaryBicone.inr_snd_assoc, neg_add_eq_zero] at hk
      obtain ⟨hk, rfl⟩ := hk
      aesop

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
⊢ IsLimit
    (ShortComplex.π₁.mapCone
      (KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))

Tactic:
apply (KernelFork.isLimitMapConeEquiv _ _).2

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
⊢ IsLimit
    ((KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯).map
      ShortComplex.π₁)
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
⊢ IsLimit
    (ShortComplex.π₂.mapCone
      (KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))

Tactic:
apply (KernelFork.isLimitMapConeEquiv _ _).2

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
⊢ IsLimit
    ((KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯).map
      ShortComplex.π₂)
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
⊢ IsLimit
    (ShortComplex.π₃.mapCone
      (KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))

Tactic:
apply (KernelFork.isLimitMapConeEquiv _ _).2

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
⊢ IsLimit
    ((KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯).map
      ShortComplex.π₃)
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsLimit (KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯)

Tactic:
by
    apply ShortComplex.isLimitOfIsLimitπ <;>
      apply (KernelFork.isLimitMapConeEquiv _ _).2
    · exact kernelIsKernel _
    · exact isLimit f g
    · exact kernelIsKernel _

Goal state after: