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

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 1 2
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₁₂ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t x ∂μ
a : A
ha : 0 ≤ a
hpcoe : ↑p ∈ Ioo 1 2
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₁₂ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p).rpowIntegrand₁₂ x 0 = 0
⊢ a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ ((↑p).rpowIntegrand₁₂ t) a ∂μ

Tactic:
calc
      a ^ p = cfcₙ (fun x => NNReal.nnrpow x p) a := by
        rw [CFC.nnrpow_def]
      _ = cfcₙ (fun r => ∫ t in Ioi 0, rpowIntegrand₁₂ p t r ∂μ) a := by
        rw [cfcₙ_nnreal_eq_real ..]
        refine cfcₙ_congr fun r hr => ?_
        have hr' : 0 ≤ r := by grind
        simp only [sup_of_le_left hr', NNReal.nnrpow_def, NNReal.coe_rpow, coe_toNNReal']
        exact (hμ r hr').2
      _ = ∫ t in Ioi 0, cfcₙ (rpowIntegrand₁₂ p t) a ∂μ :=
        cfcₙ_setIntegral measurableSet_Ioi _ bound a hf hmapzero hbound
          hbound_finite_integral ha.isSelfAdjoint

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

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

pp: case inr
b x : ℝ
hb : 1 < b
hx✝ : 0 ≤ x
hx : 0 < x
⊢ logb b x ≤ 0 ↔ x ≤ 1

Tactic:
· simp [zero_le_one]

Goal state after:
case inr
b x : ℝ
hb : 1 < b
hx✝ : 0 ≤ x
hx : 0 < x
⊢ logb b x ≤ 0 ↔ x ≤ 1
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
⊢ ConcaveOn ℝ (Ici 0) (cfcₙ (p.rpowIntegrand₀₁ t))

Tactic:
by
  apply concaveOn_cfcₙ_of_concaveOn_cfc
  refine ConcaveOn.subset (concaveOn_cfc_rpowIntegrand₀₁ hp ht) inr_map_Ici_zero ?_
  exact Convex.linear_image (convex_Ici _) (Unitization.inrHom ℝ ℂ A)

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

Goal state before:
pp: case pos.a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ ↑b ^ ⌊logb (↑b) r⌋ ≤ r

Tactic:
← rpow_intCast b

Goal state after:
case pos.a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ ↑b ^ ↑⌊logb (↑b) r⌋ ≤ r
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x y : ℝ
h : edist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ ↑1 * edist x y
⊢ dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y

Tactic:
ENNReal.coe_one,

Goal state after:
ε : ℝ
hε : 0 < ε
x y : ℝ
h : edist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ 1 * edist x y
⊢ dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ r ≤ ↑b ^ ⌈logb (↑b) r⌉

Tactic:
← rpow_intCast b

Goal state after:
case a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ r ≤ ↑b ^ ↑⌈logb (↑b) r⌉
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : MeasurableSpace E
μ : Measure E
s : Set ↑(sphere 0 1)
r : ↑(Ioi 0)
⊢ μ (Subtype.val '' ⇑(homeomorphUnitSphereProd E) ⁻¹' s ×ˢ Iio r) = μ (Ioo 0 ↑r • Subtype.val '' s)

Tactic:
rw [← image2_smul, image2_image_right, ← Homeomorph.image_symm, image_image,
    ← image_subtype_val_Ioi_Iio, image2_image_left, image2_swap, ← image_prod]
  rfl

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
⊢ ‖if ↑l = l₀ then 0 else 1 / (s - ↑l) ^ 2 - 1 / ↑l ^ 2‖ ≤ 10 * r * ‖l‖ ^ (-3)

Tactic:
split_ifs

Goal state after:
case pos
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ↑l = l₀
⊢ ‖0‖ ≤ 10 * r * ‖l‖ ^ (-3)

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

Goal state before:
pp: 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₀})ᶜ

Tactic:
split_ifs

Goal state after:
case pos
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h✝ : ↑i = l₀
⊢ DifferentiableOn ℂ (fun z ↦ 0) (↑L.lattice \ {l₀})ᶜ

case neg
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h✝ : ¬↑i = l₀
⊢ DifferentiableOn ℂ (fun z ↦ 1 / (z - ↑i) ^ 2 - 1 / ↑i ^ 2) (↑L.lattice \ {l₀})ᶜ
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case e_f
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
⊢ ((if ↑w = ↑l₀ then 0 else 1 / (z - ↑w) ^ 2 - 1 / ↑w ^ 2) + if ↑w = ↑l₀ then 1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2 else 0) =
    1 / (z - ↑w) ^ 2 - 1 / ↑w ^ 2

Tactic:
split_ifs

Goal state after:
case pos
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
h✝ : ↑w = ↑l₀
⊢ 0 + (1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2) = 1 / (z - ↑w) ^ 2 - 1 / ↑w ^ 2

case neg
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
h✝ : ¬↑w = ↑l₀
⊢ 1 / (z - ↑w) ^ 2 - 1 / ↑w ^ 2 + 0 = 1 / (z - ↑w) ^ 2 - 1 / ↑w ^ 2
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: case refine_1
a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
⊢ (fun x ↦ Polynomial.eval x (ascPochhammer ℂ (n + 1))) = fun i ↦ Polynomial.eval i (ascPochhammer ℂ n) * (i + ↑n)

pp: case refine_2
a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
⊢ ↑(n + 1)! = ↑n ! * (↑n + 1)

pp: case refine_3
a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
⊢ Multiset.map (fun x ↦ Gamma (x + ↑(n + 1))) b = Multiset.map (fun j ↦ Gamma (j + ↑n) * (j + ↑n)) b

Tactic:
· ext j
      simp [ascPochhammer_succ_right]

Goal state after:
case refine_2
a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
⊢ ↑(n + 1)! = ↑n ! * (↑n + 1)

case refine_3
a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
⊢ Multiset.map (fun x ↦ Gamma (x + ↑(n + 1))) b = Multiset.map (fun j ↦ Gamma (j + ↑n) * (j + ↑n)) b
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
⊢ ‖if ↑l = l₀ then 0 else -2 / (s - ↑l) ^ 3‖ ≤ 16 * ‖l‖ ^ (-3)

Tactic:
split_ifs

Goal state after:
case pos
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ↑l = l₀
⊢ ‖0‖ ≤ 16 * ‖l‖ ^ (-3)

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

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

Tactic:
split_ifs

Goal state after:
case pos
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h✝ : ↑i = l₀
⊢ DifferentiableOn ℂ (fun z ↦ 0) (↑L.lattice \ {l₀})ᶜ

case neg
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h✝ : ¬↑i = l₀
⊢ DifferentiableOn ℂ (fun z ↦ -2 / (z - ↑i) ^ 3) (↑L.lattice \ {l₀})ᶜ
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: 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₀})ᶜ

Tactic:
split_ifs

Goal state after:
case pos
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h✝ : ↑i = l₀
⊢ DifferentiableOn ℂ (fun z ↦ 0) (↑L.lattice \ {l₀})ᶜ

case neg
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h✝ : ¬↑i = l₀
⊢ DifferentiableOn ℂ (fun z ↦ 1 / (z - ↑i) ^ 2 - 1 / ↑i ^ 2) (↑L.lattice \ {l₀})ᶜ
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case refine_2
L : PeriodPair
l₀ : ℂ
⊢ ∀ (n : Finset ↥L.lattice),
    Set.EqOn (fun x2 ↦ ∑ i ∈ n, (fun l z ↦ if ↑l = l₀ then 0 else -2 / (z - ↑l) ^ 3) i x2)
      ((deriv ∘ fun x1 x2 ↦ ∑ i ∈ x1, (fun l z ↦ if ↑l = l₀ then 0 else 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2) i x2) n)
      (↑L.lattice \ {l₀})ᶜ

Tactic:
intro s l hl

Goal state after:
case refine_2
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
⊢ (fun x2 ↦ ∑ i ∈ s, (fun l z ↦ if ↑l = l₀ then 0 else -2 / (z - ↑l) ^ 3) i x2) l =
    (deriv ∘ fun x1 x2 ↦ ∑ i ∈ x1, (fun l z ↦ if ↑l = l₀ then 0 else 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2) i x2) s l
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

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

Tactic:
unfold regularizedGaussHGFun
  rw [regularizedGaussHGFunSeries_symm]

Goal state after:
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 (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})ᶜ

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

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

Tactic:
· intro x hx
    simp only [deriv_add_const', deriv_comp_add_const]
    rw [L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept,
      L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept, L.derivWeierstrassPExcept_add_coe]
    · simpa using hx
    · simp only [Set.mem_compl_iff, Set.mem_sdiff, SetLike.mem_coe, Set.mem_singleton_iff, not_and,
        Decidable.not_not, eq_sub_iff_add_eq] at hx ⊢
      exact fun H ↦ hx (by simpa using sub_mem H l.2)

Goal state after:
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.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: θ : ℂ
n : ℤ
⊢ eval (cos θ) (T ℂ n) = cos (↑n * θ)

Tactic:
induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp only [T_add_two, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add,
      cos_add_cos]
    push_cast
    ring_nf
  | neg_add_one n ih1 ih2 =>
    simp only [T_sub_one, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add',
      cos_add_cos]
    push_cast
    ring_nf

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

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

Tactic:
split_ifs

Goal state after:
case pos
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
h✝ : ↑w = ↑l₀
⊢ 0 + -2 / (z - ↑l₀) ^ 3 = -(2 / (z - ↑w) ^ 3)

case neg
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
h✝ : ¬↑w = ↑l₀
⊢ -2 / (z - ↑w) ^ 3 + 0 = -(2 / (z - ↑w) ^ 3)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: case inr
x : ℝ
h : x ≠ 1
h' : ¬x = -1
⊢ HasDerivWithinAt arcsin (1 / √(1 - x ^ 2)) (Iic x) x

Tactic:
exact (hasDerivAt_arcsin h' h).hasDerivWithinAt

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

Goal state before:
pp: m : ℕ
f : ℕ → ℝ := fun k ↦ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
⊢ HasSum (fun k ↦ 1 / (2 * ↑(k + 1) + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ (k + 1))
    (log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)))

Tactic:
change HasSum (fun k => f (k + 1)) _

Goal state after:
m : ℕ
f : ℕ → ℝ := fun k ↦ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
⊢ HasSum (fun k ↦ f (k + 1)) (log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this : IntegrableOn (fun x ↦ f x * √(1 - x ^ 2)⁻¹) (Set.uIoc (-1) 1) volume
⊢ Integrable f measureT

Tactic:
Set.uIoc_of_le (by norm_num)

Goal state after:
f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this : IntegrableOn (fun x ↦ f x * √(1 - x ^ 2)⁻¹) (Set.Ioc (-1) 1) volume
⊢ Integrable f measureT
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : κ > 0
hκ' : Metric.ball 1 κ ⊆ (fun x_1 ↦ x_1 * ‖z - x‖) ⁻¹' (↑(upperClosure (dist x '' (↑L.lattice \ {l₀}))))ᶜ
l : ↥L.lattice
hl : ↑l ≠ l₀
⊢ κ / 2 + 1 ∈ Metric.ball 1 κ

Tactic:
by simp [div_lt_iff₀, abs_eq_self.mpr hκ.le, hκ]

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

Goal state before:
pp: n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
this : ∫ (θ : ℝ) in 0..↑n * π, cos θ = 0
⊢ ∫ (x : ℝ), eval x (T ℝ n) ∂measureT = 0

Tactic:
rw [integral_measureT_eq_integral_cos]
    simp_rw [T_real_cos]
    rwa [integral_comp_mul_left _ (Int.cast_ne_zero.mpr hn), smul_eq_zero_iff_right (by aesop),
      mul_zero]

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

Goal state before:
pp: case inr.refine_2
n : ℕ
hn : n ≠ 0
x : ℕ
hx : x ∈ ↑(Finset.range (n + 1))
⊢ ↑x * π / ↑n ≤ π

Tactic:
rw [Finset.mem_coe, Finset.mem_range_succ_iff] at hx

Goal state after:
case inr.refine_2
n : ℕ
hn : n ≠ 0
x : ℕ
hx : x ≤ n
⊢ ↑x * π / ↑n ≤ π
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
x : ℝ
hx : x ∈ Finset.image (fun x ↦ node n x) (Finset.range (n + 1))
hPx : eval x P ≠ eval x (T ℝ ↑n)
i✝ : ℕ
hix : node n i✝ = x
hi✝ : i✝ ∈ Finset.Iic n
i : ℕ
hi : i ∈ Finset.Iic n
⊢ (-1) ^ i * eval (node n i) P ≤ 1 ^ i

Tactic:
one_pow

Goal state after:
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
x : ℝ
hx : x ∈ Finset.image (fun x ↦ node n x) (Finset.range (n + 1))
hPx : eval x P ≠ eval x (T ℝ ↑n)
i✝ : ℕ
hix : node n i✝ = x
hi✝ : i✝ ∈ Finset.Iic n
i : ℕ
hi : i ∈ Finset.Iic n
⊢ (-1) ^ i * eval (node n i) P ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
⊢ HasFPowerSeriesOnBall ℘[L - l₀] (L.weierstrassPExceptSeries l₀ x) x ↑r

Tactic:
constructor
  · apply FormalMultilinearSeries.le_radius_of_tendsto (l := 0)
    convert!
      tendsto_norm.comp
        (L.weierstrassPExceptSeries_hasSum l₀ (x + r) x ?_).summable.tendsto_atTop_zero using
      2 with i
    · simp
    · simp
    · intro l hl
      simpa [-Metric.mem_closedBall, mem_closedBall_iff_norm]
        using Set.subset_compl_comm.mp hr ⟨l.2, hl⟩
  · exact ENNReal.coe_pos.mpr hr0
  · intro z hz
    replace hz : ‖z‖ < r := by simpa using hz
    have := L.weierstrassPExceptSeries_hasSum l₀ (x + z) x
    simp only [add_sub_cancel_left] at this
    have A (l : ↥L.lattice) (hl : ↑l ≠ l₀) : r < ‖↑l - x‖ := by
      simpa [-Metric.mem_closedBall, mem_closedBall_iff_norm] using
        Set.subset_compl_comm.mp hr ⟨l.2, hl⟩
    convert! this (fun l hl ↦ hz.trans (A l hl)) with i
    rw [weierstrassPExceptSeries, FormalMultilinearSeries.ofScalars_apply_eq,
      FormalMultilinearSeries.coeff_ofScalars, smul_eq_mul]

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

Goal state before:
pp: n : ℤ
hn : n ≠ 0
x : ℝ
⊢ |eval x (T ℝ n)| ≤ 1 → |x| ≤ 1

Tactic:
by simpa using mt <| one_lt_abs_eval_T_real hn

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

Goal state before:
pp: case h
n : ℕ
⊢ Set.MapsTo (fun k ↦ (↑k + 1) * π / (↑n + 1)) (↑(Finset.range n)) (Set.Icc 0 π)

Tactic:
refine fun k hk => Set.mem_Icc.mpr ⟨by positivity, ?_⟩

Goal state after:
case h
n k : ℕ
hk : k ∈ ↑(Finset.range n)
⊢ (fun k ↦ (↑k + 1) * π / (↑n + 1)) k ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
⊢ Multipliable fun i ↦ 1 + sineTerm x i

Tactic:
by
  apply multipliable_one_add_of_summable
  have := summable_pow_div_add (x ^ 2) 2 1 Nat.one_lt_two
  simpa [sineTerm] using this

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

Goal state before:
pp: n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h1 : a * a + b * b = a'
h2 : b * (2 * a + b) = b'
⊢ a * a + b * b = a'

Tactic:
h1

Goal state after:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h1 : a * a + b * b = a'
h2 : b * (2 * a + b) = b'
⊢ a' = a'
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
x : ℂ
⊢ Summable fun n ↦ (x + (↑n + 1)) ^ (-1 - ↑k)

Tactic:
by
  apply ((summable_nat_add_iff 1).mpr (summable_int_iff_summable_nat_and_neg.mp
        (EisensteinSeries.linear_right_summable x 1 (k := k + 1) (by lia))).1).congr
  simp [← zpow_neg, sub_eq_add_neg]

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

Goal state before:
pp: 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)
⊢ Tendsto (fun n ↦ u n / ↑n) atTop (𝓝 l)

Tactic:
by
  apply tendsto_div_of_monotone_of_exists_subseq_tendsto_div u l hmono
  intro a ha
  obtain ⟨k, hk⟩ : ∃ k, c k < a := ((tendsto_order.1 clim).2 a ha).exists
  refine
    ⟨fun n => ⌊c k ^ n⌋₊, ?_,
      (tendsto_nat_floor_atTop (α := ℝ)).comp (tendsto_pow_atTop_atTop_of_one_lt (cone k)), hc k⟩
  have H : ∀ n : ℕ, (0 : ℝ) < ⌊c k ^ n⌋₊ := by
    intro n
    refine zero_lt_one.trans_le ?_
    simp only [Nat.one_le_cast, Nat.one_le_floor_iff, one_le_pow₀ (cone k).le]
  have A :
    Tendsto (fun n : ℕ => (⌊c k ^ (n + 1)⌋₊ : ℝ) / c k ^ (n + 1) * c k / (⌊c k ^ n⌋₊ / c k ^ n))
      atTop (𝓝 (1 * c k / 1)) := by
    refine Tendsto.div (Tendsto.mul ?_ tendsto_const_nhds) ?_ one_ne_zero
    · refine tendsto_nat_floor_div_atTop.comp ?_
      exact (tendsto_pow_atTop_atTop_of_one_lt (cone k)).comp (tendsto_add_atTop_nat 1)
    · refine tendsto_nat_floor_div_atTop.comp ?_
      exact tendsto_pow_atTop_atTop_of_one_lt (cone k)
  have B : Tendsto (fun n : ℕ => (⌊c k ^ (n + 1)⌋₊ : ℝ) / ⌊c k ^ n⌋₊) atTop (𝓝 (c k)) := by
    simp only [one_mul, div_one] at A
    convert! A using 1
    ext1 n
    field [(zero_lt_one.trans (cone k)).ne']
  filter_upwards [(tendsto_order.1 B).2 a hk] with n hn
  exact (div_le_iff₀ (H n)).1 hn.le

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
⊢ Epi (Φ.colonπ Ψ)

Tactic:
dsimp [colonπ]; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : HasKernels C
inst✝ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
⊢ PreservesLimit (parallelPair f 0) P.ι

Tactic:
have := P.createsKernels f
  have := P.hasLimit_parallelPair_comp_ι f
  exact preservesLimit_of_createsLimit_and_hasLimit _ _

Goal state after:
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G✝ : Type u_2
inst✝² : Monoid G✝
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
X Y : Action V H
g₁ g₂ : X ⟶ Y
h : (res V f).map g₁ = (res V f).map g₂
⊢ g₁.hom = g₂.hom

Tactic:
← res_map_hom _ f g₁,

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G✝ : Type u_2
inst✝² : Monoid G✝
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
X Y : Action V H
g₁ g₂ : X ⟶ Y
h : (res V f).map g₁ = (res V f).map g₂
⊢ ((res V f).map g₁).hom = g₂.hom
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : RightRigidCategory V
h : H
⊢ Xᘁ.ρ h = X.ρ h⁻¹ᘁ

Tactic:
rw [← SingleObj.inv_as_inv]

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : RightRigidCategory V
h : H
⊢ Xᘁ.ρ h = X.ρ (inv h)ᘁ

case x
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : RightRigidCategory V
h : H
⊢ SingleObj H

case y
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : RightRigidCategory V
h : H
⊢ SingleObj H
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : LeftRigidCategory V
h : H
⊢ (ᘁX).ρ h = ᘁX.ρ h⁻¹

Tactic:
rw [← SingleObj.inv_as_inv]

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : LeftRigidCategory V
h : H
⊢ (ᘁX).ρ h = ᘁX.ρ (inv h)

case x
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : LeftRigidCategory V
h : H
⊢ SingleObj H

case y
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : LeftRigidCategory V
h : H
⊢ SingleObj H
Module: Mathlib.CategoryTheory.Adjunction.Triple

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
⊢ G.map (t.adj₁.counit.app (H.obj X) ≫ t.rightToLeft.app X) = G.map (F.map (t.adj₂.counit.app X))

Tactic:
by simp [← cancel_epi (t.adj₁.unit.app _)]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: B : Type u
inst✝ : Quiver B
a b b✝ c✝ : B
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
ih : normalizeAux nil ((inclusionPath a b✝).obj { as := a✝¹ }) = a✝¹
| ((𝟭 (Discrete (Path a c✝))).obj { as := a✝¹.cons a✝ }).as

Tactic:
← ih

Goal state after:
B : Type u
inst✝ : Quiver B
a b b✝ c✝ : B
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
ih : normalizeAux nil ((inclusionPath a b✝).obj { as := a✝¹ }) = a✝¹
| ((𝟭 (Discrete (Path a c✝))).obj { as := (normalizeAux nil ((inclusionPath a b✝).obj { as := a✝¹ })).cons a✝ }).as
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ (α.naturality g).hom = F.map₂ η.inv ▷ α.app b ≫ (α.naturality f).hom ≫ α.app a ◁ G.map₂ η.hom

Tactic:
by
  simp [← IsIso.inv_comp_eq, ← G.map₂_inv η.inv]

Goal state after: