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

Goal state before:
pp: b : ℕ
digits : ℕ → Fin b
⊢ ofDigits digits ≤ 1

Tactic:
obtain rfl | hb := (Nat.one_le_of_lt (b_pos digits)).eq_or_lt
  · simp [ofDigits, ofDigitsTerm]
  rify at hb
  convert! Summable.tsum_mono summable_ofDigitsTerm _ (fun _ ↦ ofDigitsTerm_le)
  · simp_rw [pow_succ', mul_inv, ← inv_pow, ← mul_assoc]
    rw [tsum_mul_left, tsum_geometric_of_lt_one (by positivity) (by simp [inv_lt_one_iff₀, hb])]
    have := sub_pos.mpr hb
    field
  · simp_rw [pow_succ', mul_inv, ← inv_pow, ← mul_assoc]
    refine Summable.mul_left _ (summable_geometric_of_lt_one (by positivity) ?_)
    simp [inv_lt_one_iff₀, hb]

Goal state after:
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: m : ℤ
hm : 0 < m
p : ℕ
hp : Fact (Nat.Prime p)
Hpv : multiplicity (↑p) m % 2 = 1
⊢ multiplicity (↑p) m % 2 ≠ 0

Tactic:
rw [Hpv]; exact one_ne_zero

Goal state after:
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
n : ℕ
h : Irrational (x ^ ↑n)
⊢ Irrational x

Tactic:
rw [zpow_natCast] at h

Goal state after:
x : ℝ
n : ℕ
h : Irrational (x ^ n)
⊢ Irrational x
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: k : ℕ
⊢ (π / 2)⁻¹ * W k = (∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)) / ∫ (x : ℝ) in 0..π, sin x ^ (2 * k)

Tactic:
rw [integral_sin_pow_even, integral_sin_pow_odd, mul_div_mul_comm, ← prod_div_distrib, inv_div]

Goal state after:
k : ℕ
⊢ 2 / π * W k = 2 / π * ∏ x ∈ range k, (2 * ↑x + 2) / (2 * ↑x + 3) / ((2 * ↑x + 1) / (2 * ↑x + 2))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: case pos
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : q = 0
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (fun a ↦ a ^ ↑0) a ≤ (fun a ↦ a ^ ↑0) b

Tactic:
simp [CFC.rpow_zero a, CFC.rpow_zero b]

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

Goal state before:
pp: case inr
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : 0 < q
⊢ Monotone fun a ↦ a ^ q

Tactic:
exact monotone_nnrpow hp

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

Goal state before:
pp: case refine_2
p : ℝ
hp : p ∈ Ioo 1 2
C : ℝ≥0 := NNReal.mk (∫ (t : ℝ) in Ioi 0, (p - 1).rpowIntegrand₀₁ t 1)⁻¹ ⋯
μ : Measure ℝ := C • volume
x : ℝ
hx : x ∈ Ici 0
⊢ x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₁₂ t x ∂μ

Tactic:
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.Gaussian.PoissonSummation

Goal state before:
pp: 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)
this : ∀ (x : ℝ), -↑π / a * (↑x + I * b) ^ 2 = -↑π / a * ↑x ^ 2 + -2 * ↑π * I * b / a * ↑x + ↑π * b ^ 2 / a
⊢ (fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)) =O[cocompact ℝ] fun x ↦ |x| ^ (-2)

Tactic:
simp_rw [this]

Goal state after:
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)
this : ∀ (x : ℝ), -↑π / a * (↑x + I * b) ^ 2 = -↑π / a * ↑x ^ 2 + -2 * ↑π * I * b / a * ↑x + ↑π * b ^ 2 / a
⊢ (fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * ↑x ^ 2 + -2 * ↑π * I * b / a * ↑x + ↑π * b ^ 2 / a)) =O[cocompact ℝ]
    fun x ↦ |x| ^ (-2)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ 2 * (2 * ↑π) ^ (-s)
⊢ 2 * ↑π ≠ 0

Tactic:
by exact_mod_cast Real.two_pi_pos.ne'

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
⊢ MonotoneOn (cfcₙ (p.rpowIntegrand₀₁ t)) (Ici 0)

Tactic:
by
  intro a (ha : 0 ≤ a) b (hb : 0 ≤ b) hab
  calc
    _ = t ^ ((p : ℝ) - 1) • cfcₙ (rpowIntegrand₀₁ p 1) (t⁻¹ • a) := by
      rw [cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one hp ht a ha]
    _ ≤ t ^ ((p : ℝ) - 1) • cfcₙ (rpowIntegrand₀₁ p 1) (t⁻¹ • b) := by
      gcongr
      unfold rpowIntegrand₀₁
      simp only [Real.one_rpow, one_mul, inv_one]
      refine CFC.monotoneOn_one_sub_one_add_inv_real
        (?_ : 0 ≤ t⁻¹ • a) (?_ : 0 ≤ t⁻¹ • b) (by gcongr)
      all_goals positivity
    _ = cfcₙ (rpowIntegrand₀₁ p t) b := by
      rw [cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one hp ht b hb]

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

Goal state before:
pp: b n : ℕ
⊢ ⌈logb ↑b ↑n⌉₊ = Nat.clog b n

Tactic:
by
  obtain _ | _ | b := b
  · simp [Real.logb]
  · simp [Real.logb]
  obtain rfl | hn := eq_or_ne n 0
  · simp
  rw [← Nat.cast_inj (R := ℤ), Int.natCast_ceil_eq_ceil, ceil_logb_natCast (by simp),
    Int.clog_natCast]
  exact logb_nonneg (by simp [Nat.cast_add_one_pos]) (Nat.one_le_cast.2 (by lia))

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
f : X →ᵇ ℝ≥0
x : X
⊢ f x ≤ nndist 0 f

Tactic:
convert! nndist_coe_le_nndist x
  simp only [coe_zero, Pi.zero_apply, NNReal.nndist_zero_eq_val]

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

Goal state before:
pp: case h_meas
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
⊢ ∀ᶠ (n : ℕ) in atTop, AEStronglyMeasurable (⇑(g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n)) P

pp: case h_bound
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
⊢ ∃ C, ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) ω‖ ≤ C

pp: case h_lim
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
⊢ ∀ᵐ (ω : E) ∂P, Tendsto (fun n ↦ (g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) ω) atTop (𝓝 (ε.mulExpNegMulSq (g ω)))

Tactic:
· apply Eventually.of_forall
    exact fun n => StronglyMeasurable.aestronglyMeasurable (Continuous.stronglyMeasurable
        (Continuous.mul g.continuous ((1 + ((n : ℝ)⁻¹ • -(ε • g * g))) ^ n).continuous))

Goal state after:
case h_bound
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
⊢ ∃ C, ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) ω‖ ≤ C

case h_lim
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
⊢ ∀ᵐ (ω : E) ∂P, Tendsto (fun n ↦ (g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) ω) atTop (𝓝 (ε.mulExpNegMulSq (g ω)))
Module: Mathlib.Analysis.SpecialFunctions.Pochhammer

Goal state before:
pp: k n : ℕ
⊢ ↑k < ↑n - 1 → ↑k < ↑n

Tactic:
exact (sub_lt_self (n : ℝ) zero_lt_one).trans'

Goal state after:
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 → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
⊢ Tendsto (fun i ↦ ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))

Tactic:
by
  rcases eq_or_neBot L with rfl | hL
  · simp only [tendsto_bot]
  have obs := BoundedContinuousFunction.isBounded_range_integral μs f
  have bdd_above := BddAbove.isBoundedUnder L.univ_mem (by simpa using obs.bddAbove)
  have bdd_below := BddBelow.isBoundedUnder L.univ_mem (by simpa using obs.bddBelow)
  apply @tendsto_of_le_liminf_of_limsup_le ℝ ι _ _ _ L (fun i ↦ ∫ x, f x ∂(μs i)) (∫ x, f x ∂μ)
  · have key := h _ (f.add_norm_nonneg)
    simp_rw [f.integral_add_const ‖f‖] at key
    simp only [probReal_univ, smul_eq_mul, one_mul] at key
    have := liminf_add_const L (fun i ↦ ∫ x, f x ∂(μs i)) ‖f‖ bdd_above.isCobounded_ge bdd_below
    rwa [this, add_le_add_iff_right] at key
  · have key := h _ (f.norm_sub_nonneg)
    simp_rw [f.integral_const_sub ‖f‖] at key
    simp only [probReal_univ, smul_eq_mul, one_mul] at key
    have := liminf_const_sub L (fun i ↦ ∫ x, f x ∂(μs i)) ‖f‖ bdd_above bdd_below.isCobounded_le
    rwa [this, sub_le_sub_iff_left] at key
  · exact bdd_above
  · exact bdd_below

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

Goal state before:
pp: L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖↑l‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
r : ℝ
hr : 0 < r
hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)
⊢ ∀ᶠ (n : ↥L.lattice) in cofinite, ∀ x ∈ Metric.ball 0 r, ‖f n x‖ ≤ u r n

Tactic:
obtain ⟨R, hR⟩ := eventually_atTop.mp (hf r hr)

Goal state after:
L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖↑l‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
r : ℝ
hr : 0 < r
hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)
R : ℝ
hR : ∀ (b : ℝ), R ≤ b → ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖↑l‖ = b → ‖f l x‖ ≤ u r l
⊢ ∀ᶠ (n : ↥L.lattice) in cofinite, ∀ x ∈ Metric.ball 0 r, ‖f n x‖ ≤ u r n
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b : Multiset ℂ
h✝ : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
n : ℕ
hn : (b.toFinset.sup fun x ↦ ⌈-x.re⌉₊) + 1 ≤ n
j : ℂ
hj : j ∈ b
m : ℕ
h' : j + ↑n = -↑m
this : -j.re < ↑n
h : j = -↑m - ↑n
⊢ ↑m < 0

Tactic:
simpa [h] using this

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

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

Tactic:
rw [← (Equiv.addRight l).tsum_eq]

Goal state after:
L : PeriodPair
l₀ z : ℂ
l : ↥L.lattice
⊢ (∑' (c : ↥L.lattice), if ↑((Equiv.addRight l) c) = l₀ then 0 else -2 / (z + ↑l - ↑((Equiv.addRight l) c)) ^ 3) =
    ∑' (l_1 : ↥L.lattice), if ↑l_1 = l₀ - ↑l then 0 else -2 / (z - ↑l_1) ^ 3
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: x : ℝ
⊢ 0 < x.sigmoid

Tactic:
change 0 < (1 + exp (-x))⁻¹

Goal state after:
x : ℝ
⊢ 0 < (1 + rexp (-x))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: ⊢ range sigmoid = Ioo 0 1

Tactic:
rw [sigmoid, Subtype.range_coind, Real.range_sigmoid]
  ext
  simp

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

Goal state before:
pp: L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ -∑' (l_1 : ↥L.lattice), 2 / (z + ↑l - ↑l_1) ^ 3 = -∑' (l : ↥L.lattice), 2 / (z - ↑l) ^ 3

Tactic:
rw [← (Equiv.addRight l).tsum_eq]

Goal state after:
L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ -∑' (c : ↥L.lattice), 2 / (z + ↑l - ↑((Equiv.addRight l) c)) ^ 3 = -∑' (l : ↥L.lattice), 2 / (z - ↑l) ^ 3
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
⊢ HasSum (fun k ↦ ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))

Tactic:
have := (hasSum_geometric_of_lt_one h_nonneg ?_).mul_left (((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2)

Goal state after:
case refine_2
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
this :
  HasSum (fun i ↦ (1 / (2 * ↑(n + 1) + 1)) ^ 2 * ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ i)
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 * (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)⁻¹)
⊢ HasSum (fun k ↦ ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))

case refine_1
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
⊢ (1 / (2 * ↑(n + 1) + 1)) ^ 2 < 1
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: | Tendsto (fun n ↦ ↑n / (2 * ↑n + 1)) atTop (𝓝 (1 / 2))

Tactic:
congr
    · skip
    · skip
    rw [one_div, ← add_zero (2 : ℝ)]

Goal state after:
case l₂
| 𝓝 (2 + 0)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
P : ℝ[X]
hn : n ≠ 0
hP : P.degree < 2 * ↑n
⊢ P ∈ degreeLT ℝ (2 * n)

Tactic:
rwa [mem_degreeLT]

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 : ℕ
⊢ (box (n + 1)).disjUnion (Icc (-↑n) ↑n) ⋯ = Icc (-↑n.succ) ↑n.succ

Tactic:
by rw [disjUnion_eq_union, box_succ_union_prod]

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

Goal state before:
pp: case refine_1
n k i : ℕ
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 : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ ∀ (i : Finset ℕ), 0 ≤ ∏ a ∈ i, (x - node n a)

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

Goal state after:
case refine_2
n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ ∀ (i : Finset ℕ), 0 ≤ ∏ a ∈ i, (x - node n a)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case h₃
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∉ L.lattice
z : ℂ
i : ℕ
a✝ : ¬i = 0
⊢ (L.sumInvPow z (i + 2) - if l₀ ∈ L.lattice then ((l₀ - z) ^ (i + 2))⁻¹ else 0) = L.sumInvPow z (i + 2)

Tactic:
· simp [hl₀]

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

Goal state before:
pp: case h
z : ℍ
a b : ℤ
h0 : z ∈ verticalStrip |z.re| z.im
m : Fin 2 → ℤ
⊢ (r { coe := { re := |z.re|, im := z.im }, coe_im_pos := ⋯ })⁻¹ * ‖![m 0 + a, m 1 + b]‖⁻¹ ≤
    ‖r { coe := { re := |z.re|, im := z.im }, coe_im_pos := ⋯ }‖⁻¹ * ‖‖![m 0 + a, m 1 + b]‖⁻¹‖

Tactic:
simp [abs_of_pos (r_pos _)]

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

Goal state before:
pp: case inl
n : ℕ
hn : Even n
⊢ fib (-↑n) = (-1) ^ (n + 1) * ↑(Nat.fib n)

pp: case inr
n : ℕ
hn : Odd n
⊢ fib (-↑n) = (-1) ^ (n + 1) * ↑(Nat.fib n)

Tactic:
· simp [fib, hn, pow_add]

Goal state after:
case inr
n : ℕ
hn : Odd n
⊢ fib (-↑n) = (-1) ^ (n + 1) * ↑(Nat.fib n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
k : ℕ∞
hx : x ∈ ℂ_ℤ
⊢ ContDiffWithinAt ℂ (↑k) (fun x ↦ Complex.cos (↑π * x) / Complex.sin (↑π * x)) ℍₒ x

Tactic:
Complex.cos,

Goal state after:
x : ℂ
k : ℕ∞
hx : x ∈ ℂ_ℤ
⊢ ContDiffWithinAt ℂ (↑k) (fun x ↦ (cexp (↑π * x * I) + cexp (-(↑π * x) * I)) / 2 / Complex.sin (↑π * x)) ℍₒ x
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ MinFacHelper n 3

Tactic:
by
  refine ⟨by simp, by simp, ?_⟩
  refine (le_minFac'.mpr fun p hp hpn ↦ ?_).resolve_left (Nat.ne_of_gt (Nat.le_of_ble_eq_true h1))
  rcases hp.eq_or_lt with rfl | h
  · simp [(Nat.dvd_iff_mod_eq_zero ..).1 hpn] at h2
  · exact h

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

Goal state before:
pp: case refine_2
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
d : ℝ
hd : d > l
⊢ ∀ᶠ (b : ℕ) in atTop, u b / ↑b < d

Tactic:
obtain ⟨ε, hε, εpos⟩ : ∃ ε : ℝ, l + ε * (1 + ε + l) < d ∧ 0 < ε := by
      have L : Tendsto (fun ε => l + ε * (1 + ε + l)) (𝓝[>] 0) (𝓝 (l + 0 * (1 + 0 + l))) := by
        apply Tendsto.mono_left _ nhdsWithin_le_nhds
        exact
          tendsto_const_nhds.add
            (tendsto_id.mul ((tendsto_const_nhds.add tendsto_id).add tendsto_const_nhds))
      simp only [zero_mul, add_zero] at L
      exact (((tendsto_order.1 L).2 d hd).and self_mem_nhdsWithin).exists

Goal state after:
case refine_2
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
d : ℝ
hd : d > l
ε : ℝ
hε : l + ε * (1 + ε + l) < d
εpos : 0 < ε
⊢ ∀ᶠ (b : ℕ) in atTop, u b / ↑b < d
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: case refine_1
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
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
this : IsCofiltered (Comma L R)
a : A
⊢ ∃ c, Nonempty ((fst L R).obj c ⟶ a)

pp: case refine_2
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
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
this : IsCofiltered (Comma L R)
a : A
A' : Comma L R
s s' : (fst L R).obj A' ⟶ a
⊢ ∃ c' t, (fst L R).map t ≫ s = (fst L R).map t ≫ s'

Tactic:
· obtain ⟨b⟩ := IsCofiltered.nonempty (C := B)
    obtain ⟨X⟩ : Nonempty (CostructuredArrow L (R.obj b)) := IsCofiltered.nonempty
    exact ⟨⟨IsCofiltered.min a X.left, b, L.map (IsCofiltered.minToRight a X.left) ≫ X.hom⟩,
      ⟨IsCofiltered.minToLeft a X.left⟩⟩

Goal state after:
case refine_2
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
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
this : IsCofiltered (Comma L R)
a : A
A' : Comma L R
s s' : (fst L R).obj A' ⟶ a
⊢ ∃ c' t, (fst L R).map t ≫ s = (fst L R).map t ≫ s'
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: case refine_2
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
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
this : IsCofiltered (Comma L R)
a : A
A' : Comma L R
s s' : (fst L R).obj A' ⟶ a
⊢ ∃ c' t, (fst L R).map t ≫ s = (fst L R).map t ≫ s'

Tactic:
exact ⟨⟨_, A'.right, L.map (IsCofiltered.eqHom s s') ≫ A'.hom⟩,
      ⟨IsCofiltered.eqHom s s', 𝟙 A'.right, by simp⟩, IsCofiltered.eq_condition s s'⟩

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: 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
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : L.Initial
this : ∀ (d : T), IsCofiltered (CostructuredArrow L d)
⊢ IsCofiltered (Comma L R)

Tactic:
exact isCofiltered_of_isCofiltered_costructuredArrow L R

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
I : Type v₁
inst✝¹ : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝ : HasColimit F
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda' F).hom ≫ limit.π (F.rightOp ⋙ coyoneda) i = coyoneda.map (colimit.ι F (op i)).op

Tactic:
simp only [coyonedaOpColimitIsoLimitCoyoneda', Functor.mapIso_symm, Iso.trans_hom, Iso.symm_hom,
    Functor.mapIso_inv, Category.assoc, preservesLimitIso_hom_π, ← Functor.map_comp,
    limitRightOpIsoOpColimit_inv_comp_π]

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

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
C : Type u_3
inst✝ : Category.{v_2, u_3} C
F : C ⥤ Action V G
h : PreservesLimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
⊢ PreservesLimitsOfSize.{w₂, w₁, v_2, v_1, u_3, max (max u_1 u_2) v_1} F

Tactic:
constructor
  intro J _
  apply Action.preservesLimitsOfShape_of_preserves
  exact PreservesLimitsOfSize.preservesLimitsOfShape

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X✝ Y✝ : D
f : X✝ ⟶ Y✝
X' Y' : C
f' : X' ⟶ Y'
w✝ : Mono f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalMono f' := normalMonoOfMono f'
this : PreservesLimit (parallelPair NormalMono.g 0) L
⊢ L.map (f' ≫ NormalMono.g) = 0

Tactic:
simp [hf'.w]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X✝ Y✝ : D
f : X✝ ⟶ Y✝
X' Y' : C
f' : X' ⟶ Y'
w✝ : Epi f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalEpi f' := normalEpiOfEpi f'
this : PreservesColimit (parallelPair NormalEpi.g 0) L
⊢ L.map (NormalEpi.g ≫ f') = 0

Tactic:
simp [hf'.w]

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

Goal state before:
pp: case mk
B : Type u
inst✝ : Quiver B
a b c : B
p : Path a b
f g : Hom b c
η : f ⟶ g
η' : Hom₂ f g
⊢ normalizeAux p f = normalizeAux p g

Tactic:
apply @congr_fun _ _ fun p => normalizeAux p f

Goal state after:
case mk
B : Type u
inst✝ : Quiver B
a b c : B
p : Path a b
f g : Hom b c
η : f ⟶ g
η' : Hom₂ f g
⊢ (fun p ↦ normalizeAux p f) = fun p ↦ normalizeAux p g
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : OplaxTrans F G
θ : OplaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ 𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
      (F.map₂ β ▷ η.app b ≫ η.naturality g) ▷ θ.app b ⊗≫ η.app a ◁ θ.naturality g ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g) =
    𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
      η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (G.map₂ β ▷ θ.app b ≫ θ.naturality g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g)

Tactic:
rw [η.naturality_naturality]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : OplaxTrans F G
θ : OplaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ 𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
      (η.naturality f ≫ η.app a ◁ G.map₂ β) ▷ θ.app b ⊗≫ η.app a ◁ θ.naturality g ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g) =
    𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
      η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (G.map₂ β ▷ θ.app b ≫ θ.naturality g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g)
Module: Mathlib.CategoryTheory.Bicategory.LocallyGroupoid

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a✝ b✝ c✝ : Pith B
f✝ g✝ : a✝ ⟶ b✝
h✝ i✝ : b✝ ⟶ c✝
η : f✝ ⟶ g✝
θ : h✝ ⟶ i✝
⊢ { iso := f✝.of ◁ᵢ θ.iso } ≫ { iso := η.iso ▷ᵢ i✝.of } = { iso := η.iso ▷ᵢ h✝.of } ≫ { iso := g✝.of ◁ᵢ θ.iso }

Tactic:
by
    ext
    simp [whisker_exchange]

Goal state after: