mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ
hr : 1 ≤ 1
⊢ 0 = -0

Tactic:
neg_zero

Goal state after:
case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hr : 1 ≤ 1
⊢ 0 = 0
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 : ℕ
hb : b ≤ 1
r : R
h : r ≤ 1
⊢ -0 = 0

Tactic:
neg_zero

Goal state after:
case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
h : r ≤ 1
⊢ 0 = 0
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
hr : r ≤ 0
⊢ -0 = 0

Tactic:
neg_zero

Goal state after:
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
⊢ 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: a b : ℝ
⊢ (logb a b)⁻¹ = logb b a

Tactic:
by simp_rw [logb, inv_div]

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

Goal state before:
pp: case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ log (b ^ logb b x) = log |x|

Tactic:
rw [log_rpow b_pos, logb, log_abs]

Goal state after:
case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ log x / log b * log b = log x
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
hrp : r ≤ 0
⊢ 0 = -0

Tactic:
neg_zero

Goal state after:
case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : r ≤ 0
⊢ 0 = 0
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 : ℕ
hb : b ≤ 1
r : R
⊢ -0 = 0

Tactic:
neg_zero

Goal state after:
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
⊢ 0 = 0
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: case inr
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ Tendsto (fun i ↦ ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))

Tactic:
have bdd_below := BddBelow.isBoundedUnder L.univ_mem (by simpa using obs.bddBelow)

Goal state after:
case inr
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ Tendsto (fun i ↦ ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact (closure K) ∧ μ Kᶜ < ε
s t : Set α
hs : (IsCompact ∘ closure) s
ht : IsClosed t
this : IsCompact (closure s ∩ t)
⊢ (IsCompact ∘ closure) (s ∩ t)

Tactic:
refine this.of_isClosed_subset isClosed_closure ?_

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact (closure K) ∧ μ Kᶜ < ε
s t : Set α
hs : (IsCompact ∘ closure) s
ht : IsClosed t
this : IsCompact (closure s ∩ t)
⊢ closure (s ∩ t) ⊆ closure s ∩ t
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
key : limsup (fun i ↦ ∫ (x : X), f x ∂μs i + ‖f‖) L ≤ ∫ (x : X), f x ∂μ + ‖f‖
⊢ limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ

Tactic:
have := limsup_add_const L (fun i ↦ ∫ x, f x ∂(μs i)) ‖f‖ bdd_above bdd_below.isCobounded_le

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
key : limsup (fun i ↦ ∫ (x : X), f x ∂μs i + ‖f‖) L ≤ ∫ (x : X), f x ∂μ + ‖f‖
this : limsup (fun i ↦ ∫ (x : X), f x ∂μs i + ‖f‖) L = limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L + ‖f‖
⊢ limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) MeasurableSet

Tactic:
suffices P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s)
      fun s ↦ MeasurableSet s ∧ P s ≠ ∞ by
    convert! this
    simp only [iff_self_and]
    exact fun _ ↦ measure_ne_top P _
  refine Measure.InnerRegularWRT.measurableSet_of_isOpen ?_ ?_
  · exact innerRegularWRT_isCompact_isClosed_isOpen P
  · rintro s t ⟨hs_compact, hs_closed⟩ ht_open
    rw [sdiff_eq]
    exact ⟨hs_compact.inter_right ht_open.isClosed_compl,
      hs_closed.inter (isClosed_compl_iff.mpr ht_open)⟩

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: case inr
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ Tendsto (fun i ↦ ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))

Tactic:
have bdd_below := BddBelow.isBoundedUnder L.univ_mem (by simpa using obs.bddBelow)

Goal state after:
case inr
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ Tendsto (fun i ↦ ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))
Module: Mathlib.Analysis.SpecialFunctions.Pochhammer

Goal state before:
pp: case h0
n : ℕ
ih : MonotoneOn (deriv fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) (Set.Ioi (↑n - 1))
a : ℝ
ha : ↑n < a
b : ℝ
hb : ↑n < b
hab : a ≤ b
i : ℕ
hi : i ∈ Finset.range (n + 1)
j : ℕ
hj : j ≠ i ∧ j ∈ Finset.range (n + 1)
⊢ 0 ≤ a - ↑j

Tactic:
Finset.mem_range

Goal state after:
case h0
n : ℕ
ih : MonotoneOn (deriv fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) (Set.Ioi (↑n - 1))
a : ℝ
ha : ↑n < a
b : ℝ
hb : ↑n < b
hab : a ≤ b
i : ℕ
hi : i ∈ Finset.range (n + 1)
j : ℕ
hj : j ≠ i ∧ j < n + 1
⊢ 0 ≤ a - ↑j
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
α β : ℚ
⊢ ↑α * L.ω₁ + ↑β * L.ω₂ ∈ L.lattice ↔ α.den = 1 ∧ β.den = 1

Tactic:
refine ⟨fun H ↦ ?_, fun ⟨h₁, h₂⟩ ↦ ?_⟩
  · obtain ⟨m, n, e⟩ := mem_lattice.mp H
    have := LinearIndependent.pair_iff.mp L.indep (m - α) (n - β)
      (by simp; linear_combination e)
    simp only [sub_eq_zero] at this
    norm_cast at this
    aesop
  · lift α to ℤ using h₁
    lift β to ℤ using h₂
    simp only [Rat.cast_intCast, ← zsmul_eq_mul]
    exact add_mem (Submodule.smul_mem _ _ L.ω₁_mem_lattice)
      (Submodule.smul_mem _ _ L.ω₂_mem_lattice)

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

Goal state before:
pp: L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ∑' (b : ↥L.lattice),
      ((if ↑b = ↑l₀ then 0 else 1 / (z - ↑b) ^ 2 - 1 / ↑b ^ 2) +
        if ↑b = ↑l₀ then 1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2 else 0) =
    ℘[L] z

Tactic:
congr with w

Goal state after:
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
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) ε) * μ.real (ball 0 1) ≤ μ.toSphere.real (ball x ε)

Tactic:
Measure.real,

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
ε : ℝ
hε : 0 < ε
x : ↑(sphere 0 1)
⊢ ↑(toSphereBallBound (dim E) ε) * (μ (ball 0 1)).toReal ≤ μ.toSphere.real (ball x ε)
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)).toReal ≤ μ.toSphere.real (ball x ε)

Tactic:
Measure.real,

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
ε : ℝ
hε : 0 < ε
x : ↑(sphere 0 1)
⊢ ↑(toSphereBallBound (dim E) ε) * (μ (ball 0 1)).toReal ≤ (μ.toSphere (ball x ε)).toReal
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

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

Tactic:
by
  unfold regularizedGaussHGFunSeries
  rw [Multiset.pair_comm]

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

Goal state before:
pp: case e'_9
x : ℝ
⊢ x.sigmoid * (1 - x.sigmoid) = -(rexp (-x) * -1) / (1 + rexp (-x)) ^ 2

Tactic:
rw [← sigmoid_neg, ← sigmoid_mul_rexp_neg x, sigmoid_def]

Goal state after:
case e'_9
x : ℝ
⊢ (1 + rexp (-x))⁻¹ * ((1 + rexp (-x))⁻¹ * rexp (-x)) = -(rexp (-x) * -1) / (1 + rexp (-x)) ^ 2
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 x : ℝ
hx : (0 < x ∧ x < r) ∧ (x = 0 → dim E - 1 = 0) ∧ ¬f x = 0
⊢ x ∈ Ioi 0

Tactic:
refine mem_Ioi.mpr hx.1.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
⊢ ∫ (x : ↑{0}ᶜ), f ‖↑x‖ ∂Measure.comap Subtype.val μ =
    ∫ (x : ↑(sphere 0 1) × ↑(Ioi 0)), f ↑x.2 ∂μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1))

Tactic:
simpa using μ.measurePreserving_homeomorphUnitSphereProd.integral_comp
        (Homeomorph.measurableEmbedding _) (f ∘ Subtype.val ∘ Prod.snd)

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

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

Tactic:
cos_mul_I

Goal state after:
θ : ℂ
n : ℤ
⊢ eval (cosh θ) (T ℂ n) = eval (cosh θ) (T ℂ n)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

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

Tactic:
congr with w

Goal state after:
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)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ ℘'[L] 0 = ℘'[L] (-0)

Tactic:
neg_zero

Goal state after:
L : PeriodPair
⊢ ℘'[L] 0 = ℘'[L] 0
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₀
⊢ ∀ l ∈ L.lattice, l ≠ l₀ → (κ / 2 + 1) * ‖z - x‖ < dist x l

Tactic:
simpa using @hκ' (κ / 2 + 1) (by simp [div_lt_iff₀, abs_eq_self.mpr hκ.le, hκ])

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

Goal state before:
pp: case a
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
i : ℕ
hrange : i ∈ range (2 * n)
⊢ ∫ (a : ℝ), eval a (↑(chebyshevTsequence ℝ) i) ∂measureT = sumZeroes n (↑(chebyshevTsequence ℝ) i)

Tactic:
simp_rw [chebyshevTsequence]

Goal state after:
case a
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
i : ℕ
hrange : i ∈ range (2 * n)
⊢ ∫ (a : ℝ), eval a (T ℝ ↑i) ∂measureT = sumZeroes n (T ℝ ↑i)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case degree_g_lt
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
h : ∑ i ≤ n, eval (node n i) P * c i = ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i
⊢ (T ℝ ↑n).degree < ↑(Finset.image (fun x ↦ node n x) (Finset.range (n + 1))).card

Tactic:
rw [degree_T, Int.natAbs_natCast, Nat.cast_lt,
      Finset.card_image_of_injOn (strictAntiOn_node n).injOn,
      Finset.card_range, Nat.lt_succ_iff]

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r q : ℚ
hq : cos (↑r * π) = ↑q
⊢ cos ((↑r - ↑⌊r⌋) * π) = (-1) ^ ⌊r⌋ * ↑q

Tactic:
sub_mul,

Goal state after:
r q : ℚ
hq : cos (↑r * π) = ↑q
⊢ cos (↑r * π - ↑⌊r⌋ * π) = (-1) ^ ⌊r⌋ * ↑q
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹⁰ : Ring α
inst✝⁹ : PartialOrder α
inst✝⁸ : IsOrderedRing α
inst✝⁷ : Ring β
inst✝⁶ : PartialOrder β
inst✝⁵ : IsOrderedRing β
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : LocallyFiniteOrder β
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableLE (α × β)
n : ℕ
⊢ #(box (n + 1)) = #(Icc (-↑n.succ) ↑n.succ) * #(Icc (-↑n.succ) ↑n.succ) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n)

Tactic:
box_succ_eq_sdiff,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹⁰ : Ring α
inst✝⁹ : PartialOrder α
inst✝⁸ : IsOrderedRing α
inst✝⁷ : Ring β
inst✝⁶ : PartialOrder β
inst✝⁵ : IsOrderedRing β
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : LocallyFiniteOrder β
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableLE (α × β)
n : ℕ
⊢ #(Icc (-↑n.succ) ↑n.succ \ Icc (-↑n) ↑n) =
    #(Icc (-↑n.succ) ↑n.succ) * #(Icc (-↑n.succ) ↑n.succ) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: c d : ℝ
hc : 1 ≤ c ^ 2
z : ℂ
hz : 0 < z.im
⊢ r { coe := z, coe_im_pos := hz } ≤ ‖↑c * ↑{ coe := z, coe_im_pos := hz } + ↑d‖

Tactic:
have H1 : z.im ≤ √((c * z.re + d) ^ 2 + (c * z).im ^ 2) := by
    rw [Real.le_sqrt' hz, im_ofReal_mul, mul_pow]
    exact (le_mul_of_one_le_left (sq_nonneg _) hc).trans <| le_add_of_nonneg_left (sq_nonneg _)

Goal state after:
c d : ℝ
hc : 1 ≤ c ^ 2
z : ℂ
hz : 0 < z.im
H1 : z.im ≤ √((c * z.re + d) ^ 2 + (↑c * z).im ^ 2)
⊢ r { coe := z, coe_im_pos := hz } ≤ ‖↑c * ↑{ coe := z, coe_im_pos := hz } + ↑d‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case refine_1
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 < (-1) ^ i * (↑k.factorial * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹)

pp: case refine_2
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ ∀ i_1 ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), 0 ≤ ∏ a ∈ i_1, (x - node n a)

pp: case refine_3
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ ∃ i_1 ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), 0 < ∏ a ∈ i_1, (x - node n a)

Tactic:
· rw [← mul_assoc, mul_comm (a := (-1) ^ i), mul_assoc]
    exact mul_pos (Nat.cast_pos.mpr <| Nat.factorial_pos k) (negOnePow_mul_leadingCoeffC_pos hi)

Goal state after:
case refine_2
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ ∀ i_1 ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), 0 ≤ ∏ a ∈ i_1, (x - node n a)

case refine_3
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ ∃ i_1 ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), 0 < ∏ a ∈ i_1, (x - node n a)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

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

Tactic:
have hkn : (k : ℝ) ≤ n := by
      rw [← mul_one (n : ℝ), hk']
      gcongr
      exact div_le_one_of_le₀ (arccos_le_pi x) (by positivity)

Goal state after:
case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : ↑k * π = ↑n * arccos x
hk' : ↑k = ↑n * (arccos x / π)
hkn : ↑k ≤ ↑n
⊢ ∃ k ≤ n, x = cos (↑k * π / ↑n)
Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : CompleteSpace F
inst✝¹ : TopologicalSpace β
inst✝ : LocallyCompactSpace β
f : α → β → F
s : Set β
hs : IsOpen[inst✝¹] s
hu : ∀ K ⊆ s, IsCompact K → ∃ u, Summable u ∧ ∀ᶠ (n : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n
⊢ SummableLocallyUniformlyOn f s

Tactic:
by
  apply HasSumLocallyUniformlyOn.summableLocallyUniformlyOn (g := fun x ↦ ∑' n, f n x)
  rw [hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn,
    tendstoLocallyUniformlyOn_iff_forall_isCompact hs]
  intro K hK hKc
  obtain ⟨u, hu1, hu2⟩ := hu K hK hKc
  exact tendstoUniformlyOn_tsum_of_cofinite_eventually hu1 hu2

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

Goal state before:
pp: R : Type u_1
a b u₀ : R
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ha : 1 < a
h0 : b / (1 - a) < u₀
n : ℕ
h_lt : arithGeom a b u₀ n * (1 - a) < b
⊢ arithGeom a b u₀ n < arithGeom a b u₀ (n + 1)

Tactic:
rw [arithGeom_succ]

Goal state after:
R : Type u_1
a b u₀ : R
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ha : 1 < a
h0 : b / (1 - a) < u₀
n : ℕ
h_lt : arithGeom a b u₀ n * (1 - a) < b
⊢ arithGeom a b u₀ n < a * arithGeom a b u₀ n + b
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: ⊢ HasProdLocallyUniformlyOn (fun n z ↦ 1 + sineTerm z n) (fun x ↦ Complex.sin (↑π * x) / (↑π * x)) ℂ_ℤ

Tactic:
by
  apply hasProdLocallyUniformlyOn_of_forall_compact Complex.isOpen_compl_range_intCast
  exact fun _ hZ hZC => HasProdUniformlyOn_sineTerm_prod_on_compact hZ hZC

Goal state after:
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: n : ℤ
⊢ fib (2 * n + 2) = fib (n + 1) * (2 * fib n + fib (n + 1))

Tactic:
← mul_add_one,

Goal state after:
n : ℤ
⊢ fib (2 * (n + 1)) = fib (n + 1) * (2 * fib n + fib (n + 1))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k d : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ iteratedDerivWithin k (fun z ↦ cotTerm z d) (range Int.cast)ᶜ z =
    (fun z ↦ (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))) z

Tactic:
simpa using! eqOn_iteratedDerivWithin_cotTerm_integerComplement k d
    (coe_mem_integerComplement ⟨z, hz⟩)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
X : D
⊢ ∃ f, Epi f

Tactic:
by
  classical
  refine ⟨Sigma.desc (Pi.single X (𝟙 _)) ≫ Sigma.desc (fun f => f), ?_⟩
  have h := (isSeparator_iff_epi (projectiveSeparator C)).1
    isSeparator_projectiveSeparator (F.obj X)
  suffices Epi (Sigma.desc (Pi.single X (𝟙 _))) from epi_comp' this h
  exact SplitEpi.epi ⟨Sigma.ι (fun (X : D) => ∐ fun _ => projectiveSeparator C) X, by simp⟩

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

Goal state before:
pp: N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
this : c ^ 3 = c ^ 2 * c
⊢ c ^ 2 * (c ^ 2)⁻¹ * c ≤ c ^ 2

Tactic:
mul_inv_cancel₀ (sq_pos_of_pos cpos).ne',

Goal state after:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
this : c ^ 3 = c ^ 2 * c
⊢ 1 * c ≤ c ^ 2
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ ⌊Real.log j / Real.log c⌋₊ ≤ i

Tactic:
apply Nat.floor_le_of_le

Goal state after:
case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ Real.log j / Real.log c ≤ ↑i
Module: Mathlib.CategoryTheory.Limits.Indization.IndObject

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
⊢ IsFiltered (CostructuredArrow yoneda A) ∧ FinallySmall (CostructuredArrow yoneda A) ↔ PreservesFiniteLimits A

Tactic:
refine ⟨fun ⟨h₁, h₂⟩ => ?_, fun h => ⟨?_, ?_⟩⟩
    · apply preservesFiniteLimits_of_isFiltered_costructuredArrow_yoneda
    · exact isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits A
    · have := essentiallySmallSelf (CostructuredArrow yoneda A)
      apply finallySmall_of_essentiallySmall

Goal state after: