mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto arctan (𝓝[<] 1) (𝓝 l)
⊢ Tendsto (fun k ↦ ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))

Tactic:
tendsto_nhds_unique abel ((continuous_arctan.tendsto 1).mono_left m),

Goal state after:
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (arctan 1))
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto arctan (𝓝[<] 1) (𝓝 l)
⊢ Tendsto (fun k ↦ ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

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

Tactic:
by
  rw [← exp_injective.eq_iff, exp_arcosh hx, exp_zero]
  grind

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

Goal state before:
pp: case neg
p : ℝ
hp : p = 0 ∨ p = 1
⊢ 0 = log (1 - p) - log p

Tactic:
obtain rfl | rfl := hp

Goal state after:
case neg.inl
⊢ 0 = log (1 - 0) - log 0

case neg.inr
⊢ 0 = log (1 - 1) - log 1
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
⊢ I 1 θ * θ ^ 3 = 4 * sin θ - 4 * θ * cos θ

Tactic:
_root_.pow_succ,

Goal state after:
θ : ℝ
⊢ I 1 θ * (θ ^ 2 * θ) = 4 * sin θ - 4 * θ * cos θ
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hR : Tendsto f atTop (𝓝 R)
δ : ℝ
hδ : δ > 0
N : ℝ
hN : ∀ (b : ℝ), N ≤ b → dist (f b) R < δ
hm : 0 < min a b
t : ℝ
ht : max 1 (N / min a b) ≤ t
x : ℝ
hx : x ∈ uIoc (a * t) (b * t)
ht_pos : 0 < t
hNx : N ≤ x
hdist : ‖f x - R‖ < δ
⊢ ‖f x - R‖ ≤ δ

Tactic:
exact le_of_lt hdist

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 R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
u : ℝ → E := fun x ↦ x⁻¹ • f x
hint : ∀ {p q : ℝ}, 0 < p → 0 < q → IntervalIntegrable u volume p q
ε r : ℝ
hε : 0 < ε
hr : 0 < r
⊢ (∫ (x : ℝ) in ε..r, x⁻¹ • f (a * x)) - ∫ (x : ℝ) in ε..r, x⁻¹ • f (b * x) =
    (∫ (y : ℝ) in a * ε..a * r, u y) - ∫ (y : ℝ) in b * ε..b * r, u y

Tactic:
rw [integral_comp_mul_inv_smul ha.ne', integral_comp_mul_inv_smul hb.ne']

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

Goal state before:
pp: p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)

Tactic:
have hxt : t + x ≠ 0 := by positivity

Goal state after:
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
hxt : t + x ≠ 0
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm ((algebraMap ℝ A) t, LinearMap.id)
haddl : Function.Injective ⇑addl
⊢ Ici 0 = ⇑addl ⁻¹' ⇑addl '' Ici 0

Tactic:
Set.preimage_image_eq _ haddl

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm ((algebraMap ℝ A) t, LinearMap.id)
haddl : Function.Injective ⇑addl
⊢ Ici 0 = Ici 0
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 0 1
⊢ 0 < -1 / (2 * (p - 1))

Tactic:
rw [neg_div, neg_pos, one_div_neg]
      push _ ∈ _ at hp
      linarith

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

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 1 2
⊢ ∃ μ,
    ∀ x ∈ Ici 0,
      IntegrableOn (fun t ↦ p.rpowIntegrand₁₂ t x) (Ioi 0) μ ∧ x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₁₂ t x ∂μ

Tactic:
let C : ℝ≥0 := .mk
    (∫ t in Ioi 0, rpowIntegrand₀₁ (p - 1) t 1)⁻¹ <| by
      rw [inv_nonneg]
      exact le_of_lt <| integral_rpowIntegrand₀₁_one_pos (by grind)
  let μ : Measure ℝ := C • volume
  refine ⟨μ, fun x hx => ⟨?_, ?_⟩⟩
  · unfold μ IntegrableOn
    rw [Measure.restrict_smul]
    exact Integrable.smul_measure_nnreal <| integrableOn_rpowIntegrand₁₂ hp hx
  · rw [Measure.restrict_smul, integral_smul_nnreal_measure,
      rpow_eq_const_mul_integral_rpowIntegrand₁₂ hp hx]
    simp [C, NNReal.smul_def]

Goal state after:
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 0 1
μ : 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
a✝ : Nontrivial A
p_pos : 0 < ↑p
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)
t : ℝ
ht : t ∈ Ioi 0
z : ℝ
hz : z ∈ quasispectrum ℝ a
hz' : 0 ≤ z
⊢ ‖f t z‖ ≤ bound t

Tactic:
unfold bound f

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
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 0 1
μ : 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
a✝ : Nontrivial A
p_pos : 0 < ↑p
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)
t : ℝ
ht : t ∈ Ioi 0
z : ℝ
hz : z ∈ quasispectrum ℝ a
hz' : 0 ≤ z
⊢ ‖(↑p).rpowIntegrand₀₁ t z‖ ≤ ‖(↑p).rpowIntegrand₀₁ t maxr‖
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ deriv (fun s ↦ Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π) (1 / 2) + √π * γ =
    √π * (deriv (fun s ↦ Gamma (2 * s) * 2 ^ (1 - 2 * s)) (1 / 2) + γ)

Tactic:
mul_comm √π,

Goal state after:
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ deriv (fun s ↦ Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π) (1 / 2) + γ * √π =
    √π * (deriv (fun s ↦ Gamma (2 * s) * 2 ^ (1 - 2 * s)) (1 / 2) + γ)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ deriv (fun s ↦ Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π) (1 / 2) + γ * √π =
    √π * (deriv (fun s ↦ Gamma (2 * s) * 2 ^ (1 - 2 * s)) (1 / 2) + γ)

Tactic:
mul_comm √π,

Goal state after:
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ deriv (fun s ↦ Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π) (1 / 2) + γ * √π =
    (deriv (fun s ↦ Gamma (2 * s) * 2 ^ (1 - 2 * s)) (1 / 2) + γ) * √π
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)
t : ℝ
ht : t ∈ Ioi 0
z : ℝ
hz : z ∈ quasispectrum ℝ a
hz' : 0 ≤ z
⊢ ‖f t z‖ ≤ bound t

Tactic:
unfold bound f

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
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)
t : ℝ
ht : t ∈ Ioi 0
z : ℝ
hz : z ∈ quasispectrum ℝ a
hz' : 0 ≤ z
⊢ ‖(↑p).rpowIntegrand₁₂ t z‖ ≤ ‖(↑p).rpowIntegrand₁₂ t maxr‖
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 1 r = 0

Tactic:
by
  simp only [clog, Nat.log_one_left, Nat.cast_zero, Nat.clog_one_left, neg_zero, ite_self]

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

Goal state before:
pp: b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
⊢ ∀ (b_1 : ℝ), ∃ i, ∀ (a : ℝ), i ≤ a → logb b a ≤ b_1

Tactic:
intro e

Goal state after:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e : ℝ
⊢ ∃ i, ∀ (a : ℝ), i ≤ a → logb b a ≤ e
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, p K ∧ μ Kᶜ < ε
A : Set α
hA : q A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK : p K
hK_subset : K ⊆ A
h_lt : μ (A \ K) < μ A - r
h_lt' : μ A - μ K < μ A - r
⊢ r < μ K

Tactic:
exact lt_of_tsub_lt_tsub_left h_lt'

Goal state after:
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
μ✝ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : IsCompletelyPseudoMetrizableSpace α
inst✝ : BorelSpace α
μ : Measure α
A : Set α
hA1 : MeasurableSet A
hA2 : μ A ≠ ∞
r : ℝ≥0∞
hr : r < μ A
this : Fact (μ A < ∞)
hA2' : (μ.restrict A) A ≠ ∞
hr' : r < (μ.restrict A) A
K : Set α
hK1 : K ⊆ A
hK2 : IsCompact K
hK3 : r < (μ.restrict A) K
⊢ ∃ K ⊆ A, IsCompact K ∧ r < μ K

Tactic:
use K, hK1, hK2

Goal state after:
case right
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ✝ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : IsCompletelyPseudoMetrizableSpace α
inst✝ : BorelSpace α
μ : Measure α
A : Set α
hA1 : MeasurableSet A
hA2 : μ A ≠ ∞
r : ℝ≥0∞
hr : r < μ A
this : Fact (μ A < ∞)
hA2' : (μ.restrict A) A ≠ ∞
hr' : r < (μ.restrict A) A
K : Set α
hK1 : K ⊆ A
hK2 : IsCompact K
hK3 : r < (μ.restrict A) K
⊢ r < μ K
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✝ : μ.IsOpenPosMeasure
a✝ : Nontrivial E
U : Set ↑(sphere 0 1)
hUo : IsOpen U
hU : U.Nonempty
⊢ μ.toSphere U ≠ 0

Tactic:
μ.toSphere_apply' hUo.measurableSet

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✝ : μ.IsOpenPosMeasure
a✝ : Nontrivial E
U : Set ↑(sphere 0 1)
hUo : IsOpen U
hU : U.Nonempty
⊢ ↑(dim E) * μ (Ioo 0 1 • Subtype.val '' U) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < ↑(Module.finrank ℝ E)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
⊢ IntegrableOn f (ball 0 r) μ

Tactic:
by
  have : Nontrivial E := by
    apply Module.nontrivial_of_finrank_pos (R := ℝ)
    positivity
  have hint : IntegrableOn (fun y ↦ y ^ (Module.finrank ℝ E - 1) • (C * y ^ (-α))) (Ioo 0 r) := by
    simp only [smul_eq_mul]
    have h_rpow : IntegrableOn (fun y ↦ y ^ ((Module.finrank ℝ E : ℝ) - 1 - α)) (Ioo 0 r) := by
      by_cases! hr : 0 < r
      · rw [intervalIntegral.integrableOn_Ioo_rpow_iff hr]
        linarith
      · simp [hr]
    apply IntegrableOn.congr_fun (h_rpow.const_mul C) ?_ measurableSet_Ioo
    intro y ⟨hy, _⟩
    simp only
    move_mul [C]
    rw [← Real.rpow_natCast y (Module.finrank ℝ E - 1), ← Real.rpow_add hy]
    congr
    norm_cast
  rw [← integrableOn_fun_norm_addHaar μ] at hint
  exact Integrable.mono' hint h_meas.restrict h_decay

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

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

Tactic:
simpa using tendsto_multiset_prod _ this

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

Goal state before:
pp: L : PeriodPair
l : ↥L.lattice
⊢ ℘[L] ↑l = 0

Tactic:
← zero_add l.1,

Goal state after:
L : PeriodPair
l : ↥L.lattice
⊢ ℘[L] (0 + ↑l) = 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l : ↥L.lattice
⊢ ℘'[L] ↑l = 0

Tactic:
← zero_add l.1,

Goal state after:
L : PeriodPair
l : ↥L.lattice
⊢ ℘'[L] (0 + ↑l) = 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
⊢ deriv ℘[L] x = ℘'[L] x

Tactic:
rw [← L.weierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice,
      ← L.derivWeierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice,
      L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept (L.ω₁ / 2) (x := x) (by simp [hx])]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
n : ℕ
⊢ disjointed (fun n ↦ Icc (-↑n) ↑n) (n + 1) = Icc (-↑n.succ) ↑n.succ \ Icc (-↑n) ↑n

Tactic:
Icc_neg_mono.disjointed_add_one

Goal state after:
α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
n : ℕ
⊢ Icc (-↑(n + 1)) ↑(n + 1) \ Icc (-↑n) ↑n = Icc (-↑n.succ) ↑n.succ \ Icc (-↑n) ↑n
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
h✝ : ¬(1 ≤ i ∧ i ≤ n - k)
⊢ ∃ s ⊆ (Finset.range (n + 1)).erase i, s.card = n - k ∧ 0 ∉ s

Tactic:
exact ⟨Finset.Icc 1 (n - k), by grind, by grind [Nat.card_Icc], by simp⟩

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

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

Tactic:
· 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.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
⊢ IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x → ∃ k ≤ n, x = cos (↑k * π / ↑n)

Tactic:
intro h
    apply (abs_eval_T_real_eq_one_iff hn x).mp
    apply eq_of_le_of_ge (abs_eval_T_real_le_one n (by grind))
    refine h.elim (fun h => ?_) (fun h => ?_)
    · refine le_abs.mpr (.inr (le_neg_of_le_neg ?_))
      have := isMinOn_iff.mp h (cos (1 * π / n)) (by grind [abs_cos_le_one])
      rw [(eval_T_real_eq_neg_one_iff hn (cos (1 * π / n))).mpr ⟨1, Nat.one_le_iff_ne_zero.mpr hn,
        by simp⟩] at this
      assumption
    · refine le_abs.mpr (.inl ?_)
      have := isMaxOn_iff.mp h (cos (0 * π / n)) (by simp)
      rw [(eval_T_real_eq_one_iff hn _).mpr ⟨0, by simp, by simp⟩] at this
      assumption

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

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

Tactic:
have hn : n ≠ 0 := by grind

Goal state after:
n : ℕ
x : ℝ
hroot : x ∈ Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)
hnz : x ≠ 0
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((2 * ↑k + 1) * π / (2 * ↑n)) = x
hn : n ≠ 0
⊢ Irrational x
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2✝ : k < n.minFac
h2 : k.succ = n.minFac
⊢ k.succ % 2 = 0

Tactic:
succ_eq_add_one,

Goal state after:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2✝ : k < n.minFac
h2 : k.succ = n.minFac
⊢ (k + 1) % 2 = 0
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime k
h : MinFacHelper n k
h2 : n.minFac = k
⊢ False

Tactic:
← h2

Goal state after:
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime n.minFac
h : MinFacHelper n k
h2 : n.minFac = k
⊢ False
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n k k' : ℕ
e : k + 2 = k'
nk✝ : (n % k).beq 0 = false
h : MinFacHelper n k
h2 : n.minFac = k
nk : ¬k ∣ n
⊢ False

Tactic:
← h2

Goal state after:
n k k' : ℕ
e : k + 2 = k'
nk✝ : (n % k).beq 0 = false
h : MinFacHelper n k
h2 : n.minFac = k
nk : ¬n.minFac ∣ n
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
⊢ Summable fun n ↦ (z + ↑(-(↑n + 1))) ^ (-1 - ↑k)

Tactic:
by simpa [sub_eq_add_neg] using aux_summable_sub hk z

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x ≤ ∑ x ∈ Finset.Ico (0 + a) (b - a + a), f ↑x

Tactic:
rw [← Finset.sum_Ico_add, Nat.Ico_zero_eq_range]

Goal state after:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x ≤ ∑ x ∈ Finset.range (b - a), f ↑(a + x)
Module: Mathlib.Analysis.SpecificLimits.FloorPow

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

Tactic:
exact (tendsto_pow_atTop_atTop_of_one_lt (cone k)).comp (tendsto_add_atTop_nat 1)

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ Cᵒᵖ ⥤ Type v
hF : ∀ (i : I), IsIndObject (F.obj i)
⊢ IsIndObject (colimit F)

Tactic:
have : IsFiltered (CostructuredArrow yoneda (colimit F)) :=
    IndizationClosedUnderFilteredColimitsAux.isFiltered F hF

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ Cᵒᵖ ⥤ Type v
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
⊢ IsIndObject (colimit F)
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: case e_β
A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
A' : Type u₄
inst✝⁷ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝⁶ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝⁵ : Category.{v₆, u₆} T'
L' : A' ⥤ T'
R' : B' ⥤ T'
F : A ⥤ A'
G : B ⥤ B'
H : T ⥤ T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst✝⁴ : IsFiltered B
inst✝³ : R.Final
inst✝² : R'.Final
inst✝¹ : F.Final
inst✝ : G.Final
x✝ : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this : (R ⋙ H).Final
⊢ iR.hom =
    (G.associator R' (𝟭 T' ⋙ 𝟭 T')).inv ≫
      whiskerRight (𝟙 (G ⋙ R')) (𝟭 T' ⋙ 𝟭 T') ≫
        ((𝟭 B).associator (G ⋙ R') (𝟭 T' ⋙ 𝟭 T')).hom ≫
          (𝟭 B).whiskerLeft
              (((G ⋙ R').associator (𝟭 T') (𝟭 T')).inv ≫
                whiskerRight iR.hom (𝟭 T') ≫
                  ((𝟭 B).associator (R ⋙ H) (𝟭 T')).hom ≫ (𝟭 B).whiskerLeft (𝟙 (R ⋙ H)) ≫ ((𝟭 B).associator R H).inv) ≫
            ((𝟭 B).associator (𝟭 B ⋙ R) H).inv

Tactic:
ext; simp

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

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

Tactic:
· refine ?_ ≫ (map (colimit.ι F i)).map x
    refine homMk (𝟙 A.left) (yonedaEquiv.injective ?_)
    simp [-EmbeddingLike.apply_eq_iff_eq, hy, yonedaEquiv_comp, y']

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
⊢ HasCoseparator C

Tactic:
by
  suffices HasCoseparator (ShrinkHoms C) from
    HasCoseparator.of_equivalence (ShrinkHoms.equivalence.{w} C).symm
  obtain ⟨G, -, hG⟩ := Abelian.has_injective_coseparator (separator (ShrinkHoms C))
    (isSeparator_separator _)
  exact ⟨G, hG⟩

Goal state after: