mathlib-initiative/mathlib-tactics huggingface dataset:
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)|
⊢ ∀ᶠ (x : ℝ) in F, dist (∫ (x : ℝ) in a * x..b * x, x⁻¹ • f x) (log (b / a) • V) < δ

Tactic:
set δ' := δ / (C + 1)

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)
⊢ ∀ᶠ (x : ℝ) in F, dist (∫ (x : ℝ) in a * x..b * x, x⁻¹ • f x) (log (b / a) • V) < δ
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: 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
x : ℝ
h : x ∈ spectrum ℝ z
⊢ id x ≠ 0 ∨ 0 ≤ -1

Tactic:
have := IsStrictlyPositive.spectrum_pos (𝕜 := ℝ) zpos h

Goal state after:
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
x : ℝ
h : x ∈ spectrum ℝ z
this : 0 < x
⊢ id x ≠ 0 ∨ 0 ≤ -1
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
⊢ a + b * r ≠ 0 ∨ 0 ≤ -1

Tactic:
have : 0 ≤ b * r := by positivity

Goal state after:
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
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: 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
x : ℝ
h : x ∈ spectrum ℝ z
⊢ x ≠ 0 ∨ 0 ≤ -1

Tactic:
have := IsStrictlyPositive.spectrum_pos (𝕜 := ℝ) zpos h

Goal state after:
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
x : ℝ
h : x ∈ spectrum ℝ z
this : 0 < x
⊢ x ≠ 0 ∨ 0 ≤ -1
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

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

Tactic:
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: case refine_2
this : HasDerivAt Gamma ↑(-√π * (γ + 2 * Real.log 2)) ↑(1 / 2)
⊢ HasDerivAt Gamma (-↑√π * (↑γ + 2 * log 2)) (1 / 2)

pp: case refine_1
⊢ ∀ (m : ℕ), ↑(1 / 2) ≠ -↑m

Tactic:
· simpa only [neg_mul, one_div, ofReal_neg, ofReal_mul, ofReal_add, ofReal_ofNat, ofNat_log,
      ofReal_inv] using this

Goal state after:
case refine_1
⊢ ∀ (m : ℕ), ↑(1 / 2) ≠ -↑m
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
x : A
hx : x ∈ Ici 0
⊢ cfc (fun x ↦ t ^ (p - 1) - t ^ p * (t + x)⁻¹) x =
    (fun x ↦ (algebraMap ℝ A) (t ^ (p - 1)) - t ^ p • Ring.inverse ((algebraMap ℝ A) t + x)) x

Tactic:
have hg : ContinuousOn (fun z : ℝ => (t + z)⁻¹) (spectrum ℝ x) := by
      fun_prop (disch := grind -abstractProof)

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
x : A
hx : x ∈ Ici 0
hg : ContinuousOn (fun z ↦ (t + z)⁻¹) (spectrum ℝ x)
⊢ cfc (fun x ↦ t ^ (p - 1) - t ^ p * (t + x)⁻¹) x =
    (fun x ↦ (algebraMap ℝ A) (t ^ (p - 1)) - t ^ p • Ring.inverse ((algebraMap ℝ A) t + x)) x
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
hb : 1 < b
hr : 0 < r
⊢ r⁻¹ < ↑b ^ (log b r⁻¹ + 1)

pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ 0 < ↑b ^ (log b r⁻¹ + 1)

Tactic:
· exact lt_zpow_succ_log_self hb _

Goal state after:
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ 0 < ↑b ^ (log b r⁻¹ + 1)
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
hb : 1 < b
hx : 0 < x
⊢ 0 ≤ logb b x ↔ 1 ≤ x

Tactic:
rw [← not_lt, logb_neg_iff hb hx, not_lt]

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

Goal state before:
pp: R : Type u_1
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
r : R
⊢ clog 0 r = 0

Tactic:
by
  by_cases hr : 1 ≤ r
  · simp only [clog, Nat.clog_zero_left, Nat.cast_zero, Nat.log_zero_left, neg_zero, ite_self]
  · simp only [clog, hr, ite_cond_eq_false, Nat.log_zero_left, Nat.cast_zero, neg_zero]

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
⊢ t ^ (p - 1) • cfcₙ (p.rpowIntegrand₀₁ 1) (t⁻¹ • b) = cfcₙ (p.rpowIntegrand₀₁ t) b

Tactic:
rw [cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one hp ht b hb]

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

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

Tactic:
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.Measure.RegularityCompacts

Goal state before:
pp: case refine_2
α : 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
n : ℕ
ε : ℝ≥0∞
hε : 0 < ε
⊢ (⋃ i, f n i)ᶜ = ∅

Tactic:
h_univ,

Goal state after:
case refine_2
α : 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
n : ℕ
ε : ℝ≥0∞
hε : 0 < ε
⊢ univᶜ = ∅
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)
f : ℝ → ℝ := (Set.Ici (↑n - 1)).piecewise (fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) 0
⊢ Polynomial.eval (∑ i ∈ t, w i * ↑(p i)) (descPochhammer ℝ n) ≤ ∑ i ∈ t, w i * ↑((p i).descFactorial n)

Tactic:
suffices h_jensen : f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i) by
    simpa only [smul_eq_mul, f, Set.piecewise_eq_of_mem (Set.Ici (n - 1 : ℝ)) _ _ h_avg,
      piecewise_Ici_descPochhammer_eval_zero_eq_descFactorial] using h_jensen

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)
f : ℝ → ℝ := (Set.Ici (↑n - 1)).piecewise (fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) 0
⊢ f (∑ i ∈ t, w i • ↑(p i)) ≤ ∑ i ∈ t, w i • f ↑(p i)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ n.nthRoot 0 = 0

Tactic:
rcases n with _ | _ | _ <;> grind [nthRoot, nthRoot.go]

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
a b : ℕ
⊢ b ≤ n.nthRoot (a ^ n) ↔ b ≤ a

Tactic:
le_nthRoot_iff hn

Goal state after:
n : ℕ
hn : n ≠ 0
a b : ℕ
⊢ b ^ n ≤ a ^ n ↔ b ≤ a
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
ε : ℝ
hε : 0 < ε
x : ↑(sphere 0 1)
⊢ ↑(toSphereBallBound (dim E) ε) * μ (ball 0 1) ≤ μ.toSphere (ball x ε)

Tactic:
have : Nontrivial E := ⟨⟨x, 0, ne_of_apply_ne Norm.norm (by simp)⟩⟩
  wlog hε₂ : ε ≤ 2 generalizing ε
  · trans μ.toSphere (ball x (min ε 2))
    · simpa [Real.toNNReal_monotone.map_min, toSphereBallBound]
        using this (ε := min ε 2) (by simp [hε]) (by simp)
    · gcongr
      simp
  rw [μ.toSphere_apply' measurableSet_ball, Subtype.image_ball, ofPred_mem_eq]
  grw [← ball_subset_sector_of_small_epsilon] <;> try assumption
  · have hdim : Module.finrank ℝ E ≠ 0 := Module.finrank_pos.ne'
    have : min (ENNReal.ofReal ε) 2 = ENNReal.ofReal ε := by simpa
    simp (disch := positivity) [μ.addHaar_ball_of_pos (r := ε / 4), ENNReal.ofReal_div_of_pos,
      toSphereBallBound, mul_assoc, ENNReal.ofNNReal_toNNReal, this, hdim, hε]
  · simp

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

Goal state before:
pp: case neg
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 2 * ‖l‖ ^ 3 ≤ 16 * ‖↑l - s‖ ^ 3

pp: case neg.hb
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 0 < ‖s - ↑l‖ ^ 3

pp: case neg.hd
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 0 < ‖l‖ ^ 3

Tactic:
· refine LE.le.trans_eq (b := 2 * (2 * ‖l - s‖) ^ 3) ?_ (by ring)
    norm_cast
    gcongr
    refine le_trans ?_ (mul_le_mul le_rfl (norm_sub_norm_le _ _) (by linarith) (by linarith))
    norm_cast at *
    linarith

Goal state after:
case neg.hb
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 0 < ‖s - ↑l‖ ^ 3

case neg.hd
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 0 < ‖l‖ ^ 3
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ -2 / (l - ↑x) ^ ↑3 = deriv (fun x2 ↦ (x2 - ↑x) ^ (-↑2)) l - 0

Tactic:
Nat.cast_ofNat

Goal state after:
case neg
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ -2 / (l - ↑x) ^ 3 = deriv (fun x2 ↦ (x2 - ↑x) ^ (-2)) l - 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

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

Tactic:
rw [← L.weierstrassPExcept_add 0, Submodule.coe_zero, this, ← L.weierstrassPExcept_add (-l)]

Goal state after:
case neg
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∉ L.lattice
this : ℘[L - 0] (z + ↑l) = ℘[L - -↑l] z + -(↑l ^ 2)⁻¹
⊢ ℘[L - -↑l] z + -(↑l ^ 2)⁻¹ + (1 / (z + ↑l - 0) ^ 2 - 1 / 0 ^ 2) =
    ℘[L - ↑(-l)] z + (1 / (z - ↑(-l)) ^ 2 - 1 / ↑(-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:
let g := UniformSpace.Completion.toComplₗᵢ (𝕜 := ℝ) (E := E)

Goal state after:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
⊢ ‖f b - f a‖ₑ ≤ ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

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

Tactic:
have hz₂ : exp (k / n * π * I) = z ^ 2 := by rw [hz, ← Complex.exp_nat_mul]; grind

Goal state after:
case inr.h
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : (-1) ^ (-k) = (-1) ^ k
z : ℂ := Complex.exp (↑k / (2 * ↑n) * ↑π * I)
hz : z = Complex.exp (↑k / (2 * ↑n) * ↑π * I)
hz₂ : Complex.exp (↑k / ↑n * ↑π * I) = z ^ 2
⊢ z / (Complex.exp (↑k / ↑n * ↑π * I) - 1) + z⁻¹ / ((Complex.exp (↑k / ↑n * ↑π * I))⁻¹ - 1) = 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
H1 : (c * z.re + d) ^ 2 + (c * z.im) ^ 2 = c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2
H2 :
  (c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2) * (z.re ^ 2 + z.im ^ 2) - z.im ^ 2 =
    (c * (z.re ^ 2 + z.im ^ 2) + d * z.re) ^ 2 + (d ^ 2 - 1) * z.im ^ 2
⊢ z.im ^ 2 / (z.re ^ 2 + z.im ^ 2) ≤ c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2

Tactic:
div_le_iff₀ (by positivity),

Goal state after:
z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
H1 : (c * z.re + d) ^ 2 + (c * z.im) ^ 2 = c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2
H2 :
  (c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2) * (z.re ^ 2 + z.im ^ 2) - z.im ^ 2 =
    (c * (z.re ^ 2 + z.im ^ 2) + d * z.re) ^ 2 + (d ^ 2 - 1) * z.im ^ 2
⊢ z.im ^ 2 ≤ (c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2) * (z.re ^ 2 + z.im ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

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

Tactic:
constructor
  · intro hTx
    have hx := (abs_eval_T_real_le_one_iff (Nat.cast_ne_zero.mpr hn) x).mpr (le_of_eq hTx)
    rw [← cos_arccos (neg_le_of_abs_le hx) (le_of_max_le_left hx), T_real_cos,
      Int.cast_natCast, abs_cos_eq_one_iff] at hTx
    obtain ⟨k, hk⟩ := hTx
    have hk' : k = n * (arccos x / π) := by simpa [field]
    lift k to ℕ using (by rw [← Int.cast_nonneg_iff (R := ℝ), hk']; positivity [arccos_nonneg x])
    simp only [Int.cast_natCast] at hk hk'
    have hkn : (k : ℝ) ≤ n := by
      rw [← mul_one (n : ℝ), hk']
      gcongr
      exact div_le_one_of_le₀ (arccos_le_pi x) (by positivity)
    refine ⟨k, by simpa using hkn, ?_⟩
    convert! congr(cos ($hk.symm / n))
    rw [mul_div_cancel_left₀ _ (by simpa), cos_arccos (by grind) (by grind)]
  · rintro ⟨k, hk, rfl⟩
    rw [T_real_cos, abs_cos_eq_one_iff]
    exact ⟨k, by simp [field]⟩

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:
rw [← node_eq_one (n := n)]; exact node_lt (by grind) (by grind)

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

Goal state before:
pp: c e : ℤ
z : ℂ
⊢ (fun d ↦ ↑c * z + ↑d + ↑e) =Θ[cofinite] fun n ↦ ↑n

Tactic:
apply IsTheta.add_isLittleO

Goal state after:
case hΘ
c e : ℤ
z : ℂ
⊢ (fun d ↦ ↑c * z + ↑d) =Θ[cofinite] fun n ↦ ↑n

case ho
c e : ℤ
z : ℂ
⊢ (fun d ↦ ↑e) =o[cofinite] fun n ↦ ↑n
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: d : ℤ
z : ℂ
hz : z ≠ 0
⊢ (fun c ↦ ↑c * z + ↑d) =Θ[cofinite] fun n ↦ ↑n

Tactic:
apply IsTheta.add_isLittleO

Goal state after:
case hΘ
d : ℤ
z : ℂ
hz : z ≠ 0
⊢ (fun c ↦ ↑c * z) =Θ[cofinite] fun n ↦ ↑n

case ho
d : ℤ
z : ℂ
hz : z ≠ 0
⊢ (fun c ↦ ↑d) =o[cofinite] fun n ↦ ↑n
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: k : ℝ
hk : 2 < k
this : Summable fun n ↦ ∑' (x : ↥(box n)), ↑n ^ (-k)
⊢ Summable fun j ↦ ∑' (i : ↑↑(box j)), ‖![(↑i).1, (↑i).2]‖ ^ (-k)

Tactic:
refine this.congr fun n ↦ tsum_congr fun p ↦ ?_

Goal state after:
k : ℝ
hk : 2 < k
this : Summable fun n ↦ ∑' (x : ↥(box n)), ↑n ^ (-k)
n : ℕ
p : ↥(box n)
⊢ ↑n ^ (-k) = ‖![(↑p).1, (↑p).2]‖ ^ (-k)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case refine_1
n : ℕ
hn : n ≠ 0
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)
k : ℕ
hk : k ∈ Finset.range n
hx : cos ((↑k + 1) * π / (↑n + 1)) = x
⊢ eval (cos ((↑k + 1) * π / (↑n + 1))) (U ℝ ↑n) * sin ((↑k + 1) * π / (↑n + 1)) = 0

Tactic:
U_real_cos,

Goal state after:
case refine_1
n : ℕ
hn : n ≠ 0
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)
k : ℕ
hk : k ∈ Finset.range n
hx : cos ((↑k + 1) * π / (↑n + 1)) = x
⊢ sin ((↑↑n + 1) * ((↑k + 1) * π / (↑n + 1))) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mp.refine_2
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
h✝ : IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
h : IsMaxOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
⊢ 1 ≤ |eval x (T ℝ ↑n)|

Tactic:
refine le_abs.mpr (.inl ?_)

Goal state after:
case mp.refine_2
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
h✝ : IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
h : IsMaxOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
⊢ 1 ≤ eval x (T ℝ ↑n)
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b u₀ : R
inst✝ : Field R
ha : a ≠ 1
⊢ arithGeom a b u₀ = fun n ↦ a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)

Tactic:
ext
  exact arithGeom_eq ha _

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:
← 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.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case hbc
k : ℕ
K : Set ℂ
A B : ℝ
hB : 0 < B
hKAB : K ⊆ UpperHalfPlane.coe '' verticalStrip A B
n : ℕ
a : ℍ
haAB : a ∈ verticalStrip A B
ha : ↑a ∈ K
h1 :
  ‖↑(![1, ↑n + 1] 0) * ↑a + ↑(![1, ↑n + 1] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * ‖![1, ↑n + 1]‖ ^ (-(↑k + 1))
⊢ ‖(↑a + (↑n + 1)) ^ (-1 - ↑k) + (↑a - (↑n + 1)) ^ (-1 - ↑k)‖ ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-1 - ↑k) * |↑n + 1| ^ (-1 - ↑k) +
      r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-1 - ↑k) * |↑n + 1| ^ (-1 - ↑k)

Tactic:
have h2 := abs_norm_eq_max_natAbs_neg n ▸ summand_bound_of_mem_verticalStrip (k := k + 1)
    (by positivity) ![1, -(n + 1)] hB haAB

Goal state after:
case hbc
k : ℕ
K : Set ℂ
A B : ℝ
hB : 0 < B
hKAB : K ⊆ UpperHalfPlane.coe '' verticalStrip A B
n : ℕ
a : ℍ
haAB : a ∈ verticalStrip A B
ha : ↑a ∈ K
h1 :
  ‖↑(![1, ↑n + 1] 0) * ↑a + ↑(![1, ↑n + 1] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * ‖![1, ↑n + 1]‖ ^ (-(↑k + 1))
h2 :
  ‖↑(![1, -(↑n + 1)] 0) * ↑a + ↑(![1, -(↑n + 1)] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * (↑n + 1) ^ (-(↑k + 1))
⊢ ‖(↑a + (↑n + 1)) ^ (-1 - ↑k) + (↑a - (↑n + 1)) ^ (-1 - ↑k)‖ ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-1 - ↑k) * |↑n + 1| ^ (-1 - ↑k) +
      r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-1 - ↑k) * |↑n + 1| ^ (-1 - ↑k)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: n l : ℕ
⊢ DifferentiableOn ℂ (fun y ↦ (y + (↑n + 1)) ^ (-1 - ↑l) + (y - (↑n + 1)) ^ (-1 - ↑l)) ℍₒ

Tactic:
apply DifferentiableOn.add

Goal state after:
case hf
n l : ℕ
⊢ DifferentiableOn ℂ (fun y ↦ (y + (↑n + 1)) ^ (-1 - ↑l)) ℍₒ

case hg
n l : ℕ
⊢ DifferentiableOn ℂ (fun y ↦ (y - (↑n + 1)) ^ (-1 - ↑l)) ℍₒ
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:

Tactic:
u n / n ≤ (n * l + ε * (1 + ε + l) * n) / n := by gcongr; linarith only [hn]
      _ = (l + ε * (1 + ε + l)) := by field
      _ < d := hε

Goal state after: