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

Goal state before:
pp: case inl.inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p ∈ {0}
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ a ^ p

Tactic:
simp only [mem_singleton_iff] at hp
    simp only [hp, nnrpow_zero]
    exact concaveOn_const _ (convex_Ici _)

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 : ℝ
L : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
δ : ℝ
hδ : δ > 0
hev : ∀ᶠ (x : ℝ) in 𝓝[>] 0, dist (f x) L < δ
⊢ ∀ᶠ (t : ℝ) in 𝓝[{x | (fun t ↦ 0 < t) x}] 0, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - L‖ ≤ δ

Tactic:
rw [Filter.Eventually, mem_nhdsWithin_iff] at hev

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
δ : ℝ
hδ : δ > 0
hev : ∃ ε > 0, ball 0 ε ∩ Ioi 0 ⊆ {x | dist (f x) L < δ}
⊢ ∀ᶠ (t : ℝ) in 𝓝[{x | (fun t ↦ 0 < t) x}] 0, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - L‖ ≤ δ
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case refine_1
p : ℝ
hp : p ∈ Ioo 0 1
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun q ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
⊢ ContinuousOn g (Ioi 0 ×ˢ s)

pp: case refine_2
p : ℝ
hp : p ∈ Ioo 0 1
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun q ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
q : ℝ × ℝ
⊢ q ∈ Ioi 0 ×ˢ s → Function.uncurry p.rpowIntegrand₀₁ q = g q

Tactic:
· simp only [g]
    refine ContinuousOn.mul ?_ ?_
    · refine ContinuousOn.mul ?_ (by fun_prop)
      exact ContinuousOn.rpow_const (by fun_prop) (by grind)
    · exact ContinuousOn.inv₀ (by fun_prop) (by grind)

Goal state after:
case refine_2
p : ℝ
hp : p ∈ Ioo 0 1
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun q ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
q : ℝ × ℝ
⊢ q ∈ Ioi 0 ×ˢ s → Function.uncurry p.rpowIntegrand₀₁ q = g q
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 7 < rexp (49 / 20 - 1 / 2)

Tactic:
refine lt_of_lt_of_le ?_ (Real.sum_le_exp_of_nonneg (by norm_num) 7)

Goal state after:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 7 < ∑ i ∈ Finset.range 7, (49 / 20 - 1 / 2) ^ i / ↑i.factorial
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ (s - 1).Gammaℂ * cos (↑π * (s - 1) / 2) * (s - 1).Gammaℝ⁻¹ = s.Gammaℂ * sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹

Tactic:
(by rw [sub_add_cancel] : Gammaℂ s = Gammaℂ (s - 1 + 1)),

Goal state after:
case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ (s - 1).Gammaℂ * cos (↑π * (s - 1) / 2) * (s - 1).Gammaℝ⁻¹ = (s - 1 + 1).Gammaℂ * sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

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

Tactic:
hder_nat n,

Goal state after:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
this : -deriv f 1 = γ
⊢ deriv f 1 + ↑(harmonic n) = -γ + ↑(harmonic n)
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
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (fun x ↦ t⁻¹ • x) (Ici 0) (Ici 0)
⊢ cfcₙ (fun x ↦ p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) a = cfcₙ (p.rpowIntegrand₀₁ 1) (t⁻¹ • a)

Tactic:
refine cfcₙ_comp_smul (R := ℝ) t⁻¹ (fun x => rpowIntegrand₀₁ p 1 x) a ?_

Goal state after:
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
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (fun x ↦ t⁻¹ • x) (Ici 0) (Ici 0)
⊢ ContinuousOn (fun x ↦ p.rpowIntegrand₀₁ 1 x) ((fun x ↦ t⁻¹ • x) '' quasispectrum ℝ a)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: case e'_2
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)
Ff_bd : 𝓕 f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
⊢ ∑' (n : ℤ), cexp (-↑π * a * ↑n ^ 2 + 2 * ↑π * b * ↑n) = ∑' (n : ℤ), f (0 + ↑n)

pp: case e'_3
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)
Ff_bd : 𝓕 f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
⊢ 1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / a * (↑n + I * b) ^ 2) = ∑' (n : ℤ), 𝓕 f ↑n * (fourier n) ↑0

Tactic:
· simp only [f, zero_add, ofReal_intCast]

Goal state after:
case e'_3
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)
Ff_bd : 𝓕 f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
⊢ 1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / a * (↑n + I * b) ^ 2) = ∑' (n : ℤ), 𝓕 f ↑n * (fourier n) ↑0
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
⊢ log b r₁ ≤ log b r₂

Tactic:
rcases le_total r₂ 1 with h₂ | h₂

Goal state after:
case inl.inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
h₂ : r₂ ≤ 1
⊢ log b r₁ ≤ log b r₂

case inl.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
h₂ : 1 ≤ r₂
⊢ log b r₁ ≤ log b r₂
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : 1 ≤ r₁
⊢ log b r₁ ≤ log b r₂

Tactic:
rcases le_total r₂ 1 with h₂ | h₂

Goal state after:
case inr.inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : 1 ≤ r₁
h₂ : r₂ ≤ 1
⊢ log b r₁ ≤ log b r₂

case inr.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : 1 ≤ r₁
h₂ : 1 ≤ r₂
⊢ log b r₁ ≤ log b r₂
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
hg : ContinuousOn (fun z ↦ (t + z)⁻¹) (spectrum ℝ x)
hf : ContinuousOn (fun z ↦ 1 + z) (spectrum ℝ x)
hspectrum : ∀ r ∈ spectrum ℝ x, t + r ≠ 0
this : cfc (fun x ↦ t ^ (p - 1) - t ^ p * (t + x)⁻¹) x = cfc (fun x ↦ t ^ (p - 1)) x - cfc (fun z ↦ t ^ p * (t + z)⁻¹) x
⊢ (algebraMap ℝ A) (t ^ (p - 1)) - cfc (fun z ↦ t ^ p * (t + z)⁻¹) x =
    (fun x ↦ (algebraMap ℝ A) (t ^ (p - 1)) - t ^ p • Ring.inverse ((algebraMap ℝ A) t + x)) x

Tactic:
cfc_const_mul ..,

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)
hf : ContinuousOn (fun z ↦ 1 + z) (spectrum ℝ x)
hspectrum : ∀ r ∈ spectrum ℝ x, t + r ≠ 0
this : cfc (fun x ↦ t ^ (p - 1) - t ^ p * (t + x)⁻¹) x = cfc (fun x ↦ t ^ (p - 1)) x - cfc (fun z ↦ t ^ p * (t + z)⁻¹) x
⊢ (algebraMap ℝ A) (t ^ (p - 1)) - t ^ p • cfc (fun z ↦ (t + z)⁻¹) x =
    (fun x ↦ (algebraMap ℝ A) (t ^ (p - 1)) - t ^ p • Ring.inverse ((algebraMap ℝ A) t + x)) x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case h
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
⊢ max 1 (b ^ e) ≤ a → logb b a ≤ e

Tactic:
simp only [and_imp, sup_le_iff]

Goal state after:
case h
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
⊢ 1 ≤ a → b ^ e ≤ a → logb b a ≤ e
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
⊢ ⌈logb (↑b) r⌉ ≤ Int.clog b r

Tactic:
Int.ceil_le,

Goal state after:
case pos.a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ logb (↑b) r ≤ ↑(Int.clog b r)
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: c : ℝ
⊢ (fun x ↦ log (c * x)) =O[atTop] log

Tactic:
by
  obtain rfl | hc := eq_or_ne c 0
  · simpa using isLittleO_const_log_atTop.isBigO
  · calc (fun x ↦ log (c * x))
      =ᶠ[atTop] (fun x => log c + log x) := by
          filter_upwards [eventually_gt_atTop 0] with a ha using log_mul hc ha.ne'
      _ =O[atTop] log :=
          isLittleO_const_log_atTop.isBigO.add (Asymptotics.isBigO_refl ..)

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

Goal state before:
pp: case neg
ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left✝¹ : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
KP' : Set E
left✝ : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : P KPᶜ < ENNReal.ofReal ε
hKP' : P' KP'ᶜ < ENNReal.ofReal ε
hKPbound : P (KP ∪ KP')ᶜ < ↑ε.toNNReal
hKP'bound : P' (KP ∪ KP')ᶜ < ↑ε.toNNReal
g' : C(E, ℝ)
hg'approx : ∀ x ∈ KP ∪ KP', ‖g' x - ↑f x‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ) x = g'
g : E →ᵇ ℝ := hg'A.choose
hgA : g ∈ A
⊢ |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| ≤ 6 * √ε

Tactic:
have hgapprox : ∀ x ∈ K, ‖g x - f x‖ < √ε * const⁻¹ := by
    rw [← coe_toContinuousMapₐ ℝ g, hg'A.choose_spec.2]
    exact hg'approx

Goal state after:
case neg
ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left✝¹ : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
KP' : Set E
left✝ : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : P KPᶜ < ENNReal.ofReal ε
hKP' : P' KP'ᶜ < ENNReal.ofReal ε
hKPbound : P (KP ∪ KP')ᶜ < ↑ε.toNNReal
hKP'bound : P' (KP ∪ KP')ᶜ < ↑ε.toNNReal
g' : C(E, ℝ)
hg'approx : ∀ x ∈ KP ∪ KP', ‖g' x - ↑f x‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ) x = g'
g : E →ᵇ ℝ := hg'A.choose
hgA : g ∈ A
hgapprox : ∀ x ∈ K, ‖g x - f x‖ < √ε * const⁻¹
⊢ |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| ≤ 6 * √ε
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: case mp
n a : ℕ
hn : n ≠ 0
⊢ (∃ x, x ^ n = a) → n.nthRoot a ^ n = a

pp: case mpr
n a : ℕ
hn : n ≠ 0
⊢ n.nthRoot a ^ n = a → ∃ x, x ^ n = a

Tactic:
· rintro ⟨x, rfl⟩
    rw [nthRoot_pow hn]

Goal state after:
case mpr
n a : ℕ
hn : n ≠ 0
⊢ n.nthRoot a ^ n = a → ∃ x, x ^ n = a
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: n : ℕ
a : Multiset ℂ
hn : n ≠ 0
⊢ (Multiset.map (fun x ↦ x + ↑n) a).prod = (Multiset.map (fun j ↦ ↑n * (j / ↑n + 1)) a).prod

Tactic:
congr; ext; field_simp

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

Goal state before:
pp: a b : Multiset ℂ
n : ℕ
j : ℂ
ha : j ∈ a
hj : j = -↑n
⊢ (regularizedHGFunSeries a b).radius = ⊤

Tactic:
by
  apply FormalMultilinearSeries.radius_eq_top_of_eventually_eq_zero
  apply eventually_atTop.mpr
  use n + 1
  grind

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

Goal state before:
pp: a : Multiset ℂ
⊢ Tendsto (fun n ↦ (Multiset.map (fun x ↦ x / ↑n + 1) a).prod) atTop (𝓝 1)

Tactic:
suffices ∀ i ∈ a, Tendsto (fun n : ℕ ↦ (i / n + 1)) atTop (𝓝 <| (fun _ : _ ↦ 1) i) by
    simpa using tendsto_multiset_prod _ this
  intro i hi
  simpa using (tendsto_const_div_atTop_nhds_zero_nat i).add_const 1

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ Integrable ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) volume ↔
    IntegrableOn (fun y ↦ y ^ (dim E - 1) • f y) (Ioo 0 r) volume

Tactic:
← integrable_indicator_iff measurableSet_Ioo,

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ Integrable ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) volume ↔
    Integrable ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) volume
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : x < 1
⊢ 0 < 1 - x ^ 2

Tactic:
nlinarith [h₁, h₂]

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

Goal state before:
pp: case e'_5
m : ℕ
f : ℕ → ℝ := fun k ↦ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
⊢ f = fun i ↦ (↑(m + 1) + 1 / 2) * (2 * (1 / (2 * ↑i + 1)) * (1 / (2 * (↑m + 1) + 1)) ^ (2 * i + 1))

Tactic:
ext k
    dsimp only [f]
    rw [← pow_mul, pow_add]
    push_cast
    field

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

Goal state before:
pp: case neg
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
e : ¬↑l = l₀
⊢ (↑i + 2) * (((↑l - x) ^ (i + 3))⁻¹ - 0) = (↑(i + 1) + 1) * ((↑l - x) ^ ↑(i + 1 + 2))⁻¹ - 0 i

Tactic:
dsimp

Goal state after:
case neg
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
e : ¬↑l = l₀
⊢ (↑i + 2) * (((↑l - x) ^ (i + 3))⁻¹ - 0) = (↑(i + 1) + 1) * ((↑l - x) ^ (↑i + 1 + 2))⁻¹ - 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: n : ℤ
hn✝ : n ≠ 0
hn' : ↑n ≠ 0
hn : n < 0
⊢ ∫ (θ : ℝ) in 0..↑n * π, deriv sin θ = 0

Tactic:
rw [integral_symm, integral_deriv_of_contDiffOn_Icc contDiff_sin.contDiffOn]
    · simp
    exact mul_nonpos_of_nonpos_of_nonneg (Int.cast_nonpos.mpr <| le_of_lt hn) pi_nonneg

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

Goal state before:
pp: case a
n : ℕ
k : ℤ
hn : n ≠ 0
hk : Complex.exp (↑k / ↑n * ↑π * I) = 1
m : ℤ
hx : ↑k / ↑n * ↑π * I = ↑m * (2 * ↑π * I)
⊢ ↑k + ↑m * (2 * ↑π * I) * (↑n / ↑π / I) - (↑(2 * ↑n * m) + ↑k / ↑n * ↑π * I * (↑n / ↑π / I)) = 0

Tactic:
push_cast; field [show (n : ℂ) ≠ 0 by aesop]

Goal state after:
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₀})ᶜ
z : ℂ
hz : z ∈ Metric.eball 0 ↑r
⊢ ‖z‖ < ↑r

Tactic:
simpa using hz

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

Goal state before:
pp: case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hTx : |cos (↑n * arccos x)| = 1
hx : |x| ≤ 1
⊢ ∃ k ≤ n, x = cos (↑k * π / ↑n)

Tactic:
abs_cos_eq_one_iff

Goal state after:
case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hTx : ∃ k, ↑k * π = ↑n * arccos x
hx : |x| ≤ 1
⊢ ∃ k ≤ n, x = cos (↑k * π / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mpr
n : ℕ
hn : n ≠ 0
k : ℕ
hk : k ≤ n
⊢ |cos (↑↑n * (↑k * π / ↑n))| = 1

Tactic:
abs_cos_eq_one_iff

Goal state after:
case mpr
n : ℕ
hn : n ≠ 0
k : ℕ
hk : k ≤ n
⊢ ∃ k_1, ↑k_1 * π = ↑↑n * (↑k * π / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case refine_1
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
x : ℝ
hx : x ∈ Set.Ioo (-1) 1
⊢ (fun x ↦ eval x (T ℝ ↑n)) x ≤ (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n))

Tactic:
dsimp

Goal state after:
case refine_1
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
x : ℝ
hx : x ∈ Set.Ioo (-1) 1
⊢ eval x (T ℝ ↑n) ≤ eval (cos (↑k * π / ↑n)) (T ℝ ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case refine_3
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ cos (↑k * π / ↑n) < 1

Tactic:
rw [← cos_zero]

Goal state after:
case refine_3
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ cos (↑k * π / ↑n) < cos 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case refine_1
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
x : ℝ
hx : x ∈ Set.Ioo (-1) 1
⊢ (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n)) ≤ (fun x ↦ eval x (T ℝ ↑n)) x

Tactic:
dsimp

Goal state after:
case refine_1
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
x : ℝ
hx : x ∈ Set.Ioo (-1) 1
⊢ eval (cos (↑k * π / ↑n)) (T ℝ ↑n) ≤ eval x (T ℝ ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case refine_3
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ cos (↑k * π / ↑n) < 1

Tactic:
rw [← cos_zero]

Goal state after:
case refine_3
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ cos (↑k * π / ↑n) < cos 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case refine_2
Z : Set ℂ
hZ : IsCompact Z
hf : ContinuousOn (fun x ↦ ‖-x ^ 2‖) Z
s : ℝ
hs : ∀ y ∈ (fun x ↦ ‖-x ^ 2‖) '' Z, y ≤ s
⊢ ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ (fun n ↦ ‖↑s / (↑n + 1) ^ 2‖) j

Tactic:
simp only [norm_neg, norm_pow, Set.mem_image, forall_exists_index, and_imp,
      forall_apply_eq_imp_iff₂, sineTerm, norm_div, norm_real, norm_eq_abs] at *

Goal state after:
case refine_2
Z : Set ℂ
hZ : IsCompact Z
s : ℝ
hf : ContinuousOn (fun x ↦ ‖x‖ ^ 2) Z
hs : ∀ a ∈ Z, ‖a‖ ^ 2 ≤ s
⊢ ∀ (j : ℕ), ∀ z ∈ Z, ‖z‖ ^ 2 / ‖↑j + 1‖ ^ 2 ≤ |s| / ‖↑j + 1‖ ^ 2
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case ofNat
n : ℕ
⊢ fib (ofNat n + 2) = fib (ofNat n) + fib (ofNat n + 1)

Tactic:
dsimp

Goal state after:
case ofNat
n : ℕ
⊢ fib (↑n + 2) = ↑(Nat.fib n) + fib (↑n + 1)
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
⊢ Epi { X₁ := X, X₂ := X ⊞ Y, X₃ := Y, f := biprod.inl, g := biprod.snd, zero := ⋯ }.g

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Epi biprod.snd
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
⊢ Mono { X₁ := Y, X₂ := Y ⊞ Z, X₃ := Z, f := biprod.inl, g := biprod.snd, zero := ⋯ }.f

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Mono biprod.inl
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
⊢ Mono
    ((kernelCokernelCompSequence f g).map' 0 1 instMonoMap'KernelCokernelCompSequenceOfNatNat._proof_2
      instMonoMap'KernelCokernelCompSequenceOfNatNat._proof_4)

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Mono (kernel.map f (f ≫ g) (𝟙 X) g ⋯)
Module: Mathlib.CategoryTheory.Limits.FunctorToTypes

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ Type w
k : K
t : Cocone F
h : IsColimit t
x : t.pt.obj k
inst✝ : ∀ (k : K), HasColimit (F.flip.obj k)
⊢ ∃ j y, x = (ConcreteCategory.hom ((t.ι.app j).app k)) y

Tactic:
let hev := isColimitOfPreserves ((evaluation _ _).obj k) h

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ Type w
k : K
t : Cocone F
h : IsColimit t
x : t.pt.obj k
inst✝ : ∀ (k : K), HasColimit (F.flip.obj k)
hev : IsColimit (((evaluation K (Type w)).obj k).mapCocone t) := isColimitOfPreserves ((evaluation K (Type w)).obj k) h
⊢ ∃ j y, x = (ConcreteCategory.hom ((t.ι.app j).app k)) y
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊

Tactic:
rcases eq_or_ne i 0 with (rfl | hi)

Goal state after:
case inl
c : ℝ
hc : 1 < c
cpos : 0 < c
⊢ (1 - c⁻¹) * c ^ 0 ≤ ↑⌊c ^ 0⌋₊

case inr
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i ≠ 0
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊