mathlib-initiative/mathlib-tactics huggingface dataset:
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 : 1 < b
r : R
hr : 0 < r
⊢ r ≤ ↑b ^ (-log b r⁻¹)

Tactic:
zpow_neg,

Goal state after:
case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ r ≤ (↑b ^ log b r⁻¹)⁻¹
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
hb : 1 < b
hr : 0 < r
⊢ ↑b ^ (-(log b r⁻¹ + 1)) < r

Tactic:
zpow_neg,

Goal state after:
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ (↑b ^ (log b r⁻¹ + 1))⁻¹ < r
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₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₀' : 0 < r₂
⊢ log b r₂⁻¹ ≤ log b r₁⁻¹

Tactic:
exact log_mono_right (inv_pos_of_pos h₀') <| (inv_le_inv₀ h₀' h₀).2 h

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

Goal state before:
pp: case inr
b a c : ℝ
n : ℕ
ha : a ≠ 0
h : log b ≠ 0
⊢ Tendsto (fun x ↦ logb b x ^ n / (a * x + c)) atTop (𝓝 0)

Tactic:
apply (tendsto_pow_log_div_mul_add_atTop (a * (log b) ^ n) (c * (log b) ^ n) n
                (by positivity)).congr fun x ↦ by simp [field, div_pow, logb]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
a✝ : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
s' : ℕ → ℝ≥0∞ → ℕ
s'bound : ∀ (n : ℕ) (ε : ℝ≥0∞), 0 < ε → P (⋂ m', ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε
δ : ℕ → ℝ≥0∞
hδ1 : ∀ (i : ℕ), 0 < δ i
hδ2 : ∑' (i : ℕ), δ i < ε
u : ℕ → ℕ := fun n ↦ s' n (δ n)
⊢ P (interUnionBalls seq u t)ᶜ < ε

Tactic:
rw [interUnionBalls, Set.compl_iInter]

Goal state after:
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
a✝ : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
s' : ℕ → ℝ≥0∞ → ℕ
s'bound : ∀ (n : ℕ) (ε : ℝ≥0∞), 0 < ε → P (⋂ m', ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε
δ : ℕ → ℝ≥0∞
hδ1 : ∀ (i : ℕ), 0 < δ i
hδ2 : ∑' (i : ℕ), δ i < ε
u : ℕ → ℕ := fun n ↦ s' n (δ n)
⊢ P (⋃ i, (⋃ m, ⋃ (_ : m ≤ u i), UniformSpace.ball (seq m) (Prod.swap ⁻¹' t i))ᶜ) < ε
Module: Mathlib.Analysis.SpecialFunctions.Pochhammer

Goal state before:
pp: case succ
n : ℕ
ih : MonotoneOn (deriv fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) (Set.Ioi (↑n - 1))
a : ℝ
ha : a ∈ Set.Ioi (↑(n + 1) - 1)
b : ℝ
hb : b ∈ Set.Ioi (↑(n + 1) - 1)
hab : a ≤ b
⊢ deriv (fun x ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) a ≤
    deriv (fun x ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) b

Tactic:
rw [Set.mem_Ioi, Nat.cast_add_one, add_sub_cancel_right] at ha hb

Goal state after:
case succ
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
⊢ deriv (fun x ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) a ≤
    deriv (fun x ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) b
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

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

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

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

Goal state before:
pp: case refine_1
L : PeriodPair
α β : ℚ
H : ↑α * L.ω₁ + ↑β * L.ω₂ ∈ L.lattice
m n : ℤ
e : ↑m * L.ω₁ + ↑n * L.ω₂ = ↑α * L.ω₁ + ↑β * L.ω₂
this : ↑m = α ∧ ↑n = β
⊢ α.den = 1 ∧ β.den = 1

Tactic:
aesop

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

Goal state before:
pp: ⊢ Tendsto sigmoid atTop (𝓝 1)

Tactic:
simpa using! Real.tendsto_exp_comp_nhds_zero.mpr tendsto_neg_atTop_atBot |>.const_add 1 |>.inv₀ <|
    by norm_num

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

Goal state before:
pp: L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ (if i + 1 = 0 then ℘[L - l₀] x else (↑(i + 1) + 1) * (L.sumInvPow x (i + 1 + 2) - ((l₀ - x) ^ (i + 1 + 2))⁻¹)) =
    (↑i + 2) * (L.sumInvPow x (i + 3) - (l₀ - x) ^ (-↑(i + 3)))

Tactic:
zpow_neg,

Goal state after:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ (if i + 1 = 0 then ℘[L - l₀] x else (↑(i + 1) + 1) * (L.sumInvPow x (i + 1 + 2) - ((l₀ - x) ^ (i + 1 + 2))⁻¹)) =
    (↑i + 2) * (L.sumInvPow x (i + 3) - ((l₀ - x) ^ ↑(i + 3))⁻¹)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: x : ℝ
hx : x ∈ Set.Ioo (min (-1) 1) (max (-1) 1)
⊢ x ≠ -1

Tactic:
aesop

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

Goal state before:
pp: x : ℝ
hx : x ∈ Set.Ioo (min (-1) 1) (max (-1) 1)
⊢ x ≠ 1

Tactic:
aesop

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

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
hx : x ∈ uIcc 1 (-1)
⊢ -1 ≤ x

Tactic:
aesop

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

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
hx : x ∈ uIcc 1 (-1)
⊢ x ≤ 1

Tactic:
aesop

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

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
hx : x ∈ Ioo (min 1 (-1)) (max 1 (-1))
⊢ x ≠ -1

Tactic:
aesop

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

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
hx : x ∈ Ioo (min 1 (-1)) (max 1 (-1))
⊢ x ≠ 1

Tactic:
aesop

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

Goal state before:
pp: n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
this : ∫ (θ : ℝ) in 0..↑n * π, cos θ = 0
⊢ (↑n)⁻¹ ≠ 0

Tactic:
aesop

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

Goal state before:
pp: n : ℕ
⊢ node n 0 = 1

Tactic:
by simp [node]

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ ↑n * π / ↑n = π

Tactic:
aesop

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

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

Tactic:
aesop

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

Goal state before:
pp: n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
⊢ ↑n ≠ 0

Tactic:
aesop

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

Goal state before:
pp: n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : ∑ i ∈ range n, 2 * cos (↑k * ((2 * ↑i + 1) / (2 * ↑n) * π)) = 0
⊢ π / ↑n ≠ 0

Tactic:
aesop

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

Goal state before:
pp: n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : ∑ i ∈ range n, 2 * Complex.cos (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π)) = 0
⊢ ∑ i ∈ range n, 2 * ↑(cos (↑k * ((2 * ↑i + 1) / (2 * ↑n) * π))) = 0

Tactic:
aesop

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

Goal state before:
pp: case inr
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
⊢ ∑ i ∈ range n, 2 * Complex.cos (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π)) = 0

Tactic:
simp_rw [Complex.two_cos, ← neg_mul, ← Int.cast_neg]

Goal state after:
case inr
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
⊢ ∑ x ∈ range n,
      (Complex.exp (↑k * ((2 * ↑x + 1) / (2 * ↑n) * ↑π) * I) +
        Complex.exp (↑(-k) * ((2 * ↑x + 1) / (2 * ↑n) * ↑π) * I)) =
    0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : (-1) ^ (-k) = (-1) ^ k
⊢ ¬2 * ↑n ∣ -k

Tactic:
aesop

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

Goal state before:
pp: n : ℕ
P : ℝ[X]
hn : n ≠ 0
hP : P.degree < 2 * ↑n
⊢ ∫ (x : ℝ), eval x P ∂measureT = sumZeroes n P

Tactic:
have hmem : P ∈ degreeLT ℝ (2 * n) := by rwa [mem_degreeLT]

Goal state after:
n : ℕ
P : ℝ[X]
hn : n ≠ 0
hP : P.degree < 2 * ↑n
hmem : P ∈ degreeLT ℝ (2 * n)
⊢ ∫ (x : ℝ), eval x P ∂measureT = sumZeroes n P
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case h₂
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice := ⋯
⊢ Summable (((Function.uncurry fun b c ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b) ∘ ⇑e.symm) ∘ Sum.inr)

Tactic:
· -- for the remaining terms, we bound it by `(i + 2) κ⁻ⁱ * ‖l - x‖⁻³ * ‖z - x‖`.
    dsimp [e, Function.comp_def, Function.uncurry_def, Denumerable.eqv, weierstrassPExceptSummand]
    have H₁ : Summable fun i : ℕ ↦ ((i + 2) * κ ^ (-i : ℤ)) := by
      have : |κ⁻¹| < 1 := by grind [abs_inv, inv_lt_one_iff₀]
      simpa [mul_comm] using ((Real.hasFPowerSeriesOnBall_ofScalars_mul_add_zero 1 2).hasSum
        (y := κ⁻¹) (by simpa [enorm_eq_nnnorm])).summable
    have H₂ : Summable fun l : L.lattice ↦ ‖l - x‖ ^ (-3 : ℤ) * ‖z - x‖ :=
      (ZLattice.summable_norm_sub_zpow _ _ (by simp) _).mul_right _
    refine (H₁.mul_of_nonneg H₂ (by intro; positivity) (by intro; positivity)).of_norm_bounded ?_
    intro p
    split_ifs with hp
    · simp only [zero_mul, norm_zero, zpow_neg, zpow_natCast, Int.reduceNeg]; positivity
    have hpx : ‖p.2 - x‖ ≠ 0 := fun h ↦ by
      obtain rfl : p.2 = x := by simpa [sub_eq_zero] using h
      simpa [(norm_nonneg _).not_gt] using hx p.2 hp
    obtain rfl | hxz := eq_or_ne z x
    · simp
    calc
      _ = ‖(p.1 + 2 : ℂ)‖ * ‖p.2 - x‖ ^ (-3 - p.1 : ℤ) * ‖z - x‖ ^ (p.1 + 1) := by
        norm_num; ring_nf; simp
      _ = ‖(p.1 + 2 : ℂ)‖ * ((‖↑p.2 - x‖ / ‖z - x‖) ^ p.1)⁻¹ * ((‖p.2 - x‖ ^ 3)⁻¹ * ‖z - x‖) := by
        simp [hpx, zpow_sub₀, div_pow]; field
      _ ≤ (p.1 + 2) * (κ ^ p.1)⁻¹ * ((‖p.2 - x‖ ^ 3)⁻¹ * ‖z - x‖) := by
        gcongr
        · norm_cast
        · exact (le_div_iff₀ (by simpa [sub_eq_zero])).mpr ((mul_comm _ _).trans_le (hκ' p.2 hp).le)
      _ = _ := by simp [zpow_ofNat]

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

Goal state before:
pp: z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
⊢ r1 z ≤ (c * z.re + d) ^ 2 + (c * z.im) ^ 2

Tactic:
have H1 : (c * z.re + d) ^ 2 + (c * z.im) ^ 2 =
    c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2 := by ring
  have H2 : (c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2) * (z.re ^ 2 + z.im ^ 2)
    - z.im ^ 2 = (c * (z.re ^ 2 + z.im ^ 2) + d * z.re) ^ 2 + (d ^ 2 - 1) * z.im ^ 2 := by ring
  rw [r1, H1, div_le_iff₀ (by positivity), ← sub_nonneg, H2]
  exact add_nonneg (sq_nonneg _) (mul_nonneg (sub_nonneg.mpr hd) (sq_nonneg _))

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

Goal state before:
pp: case a
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ r1 { coe := { re := A, im := B }, coe_im_pos := h } ≤ r1 z

Tactic:
simp only [r1_eq, div_pow, one_div]

Goal state after:
case a
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ ({ coe := { re := A, im := B }, coe_im_pos := h }.re ^ 2 / { coe := { re := A, im := B }, coe_im_pos := h }.im ^ 2 +
        1)⁻¹ ≤
    (z.re ^ 2 / z.im ^ 2 + 1)⁻¹
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case refine_2
x : Fin 2 → ℤ
hx : x ≠ 0
H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs
this : x 1 ≠ 0
⊢ 1 ≤ (↑(x 1) / ‖x‖) ^ 2

Tactic:
simp only [norm_eq_max_natAbs, H1, Nat.cast_natAbs, Int.cast_abs, div_pow, sq_abs, ne_eq,
      OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, Int.cast_eq_zero, this, div_self,
      le_refl]

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

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

Tactic:
· rintro ⟨k, hk, rfl⟩
    rw [T_real_cos, abs_cos_eq_one_iff]
    exact ⟨k, by simp [field]⟩

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ Set.InjOn (fun k ↦ (2 * ↑k + 1) * π / (2 * ↑n)) ↑(Finset.range n)

Tactic:
aesop

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

Goal state before:
pp: k : ℝ
hk : 2 < k
⊢ Summable fun x ↦ ‖x‖ ^ (-k)

Tactic:
rw [← (finTwoArrowEquiv _).symm.summable_iff, summable_partition _ Int.existsUnique_mem_box]

Goal state after:
k : ℝ
hk : 2 < k
⊢ (∀ (j : ℕ), Summable fun i ↦ ((fun x ↦ ‖x‖ ^ (-k)) ∘ ⇑(finTwoArrowEquiv ℤ).symm) ↑i) ∧
    Summable fun j ↦ ∑' (i : ↑↑(box j)), ((fun x ↦ ‖x‖ ^ (-k)) ∘ ⇑(finTwoArrowEquiv ℤ).symm) ↑i

k : ℝ
hk : 2 < k
⊢ 0 ≤ (fun x ↦ ‖x‖ ^ (-k)) ∘ ⇑(finTwoArrowEquiv ℤ).symm
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n k : ℕ
hk : k < n
⊢ rootMultiplicity (cos ((2 * ↑k + 1) * π / (2 * ↑n))) (T ℝ ↑n) = 1

Tactic:
by
  rw [← count_roots, roots_T_real, Multiset.count_eq_one_of_mem (by simp)]
  grind

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

Goal state before:
pp: case hf
n x : ℕ
hx : x ∈ ↑(Finset.range n)
y : ℕ
hy : y ∈ ↑(Finset.range n)
hxy : ↑x + 1 = ↑y + 1
⊢ x = y

Tactic:
aesop

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

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
x : ℝ
hx : ↑n * eval x (U ℝ (↑n - 1)) = 0
⊢ ↑n ≠ 0

Tactic:
aesop

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

Goal state before:
pp: case mp
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : x ∈ (U ℝ (↑n - 1)).roots
⊢ ∃ k ∈ Finset.Ioo 0 n, x = cos (↑k * π / ↑n)

Tactic:
rw [show (n - 1 : ℤ) = (n - 1 : ℕ) by grind, roots_U_real, Finset.mem_val] at hx

Goal state after:
case mp
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑(n - 1) + 1))) (Finset.range (n - 1))
⊢ ∃ k ∈ Finset.Ioo 0 n, x = cos (↑k * π / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
this : x ^ 2 ≠ ↑(↑n + 1) ^ 2
⊢ ¬1 * (↑n + 1) ^ 2 = - -x ^ 2

Tactic:
aesop

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: Z : Set ℂ
hZ2 : Z ⊆ ℂ_ℤ
hZC : IsCompact Z
x : ℂ
hx : x ∈ Z
⊢ x ∈ ℂ_ℤ

Tactic:
aesop

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
k : ℤ
⊢ x ≠ ↑k

Tactic:
aesop

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
i : ℕ
h1 : x + ↑(↑i + 1) ≠ 0
h2 : x - (↑i + 1) ≠ 0
this : x ^ 2 ≠ ↑(↑i + 1) ^ 2
⊢ (↑i + 1) ^ 2 ≠ x ^ 2

Tactic:
aesop

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
n : ℕ
| ‖(↑n + 1) ^ (-↑(1 + k))‖

Tactic:
zpow_neg,

Goal state after:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
n : ℕ
| ‖((↑n + 1) ^ ↑(1 + k))⁻¹‖
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: α : Type u_1
inst✝ : CommSemiring α
⊢ fibRec.IsSolution fun x ↦ ↑(Nat.fib x)

Tactic:
by
  rw [fibRec]
  intro n
  simp only
  rw [Nat.fib_add_two, add_comm]
  simp [Finset.sum_fin_eq_sum_range, Finset.sum_range_succ']

Goal state after:
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
⊢ biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) ≫ biprod.snd = biprod.snd ≫ g

Tactic:
aesop

Goal state after:
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
⊢ biprod.lift (kernel.ι (f ≫ g)) (kernel.ι (f ≫ g) ≫ f) ≫ biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) = 0

Tactic:
aesop

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

Goal state before:
pp: case hbc
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
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ u (c b) - ↑(c b) * l ≤ ε * ↑(c b)
M : ℕ := ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := ⋯
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
IcN : ↑(c N) ≤ (1 + ε) * ↑(c (N - 1))
⊢ ↑(c N) - ↑(c (N - 1)) ≤ ε * ↑(c (N - 1))

Tactic:
linarith only [IcN]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k₁ : A ⟶ X
hk : (k₁ ≫ f) ≫ g = 0
⊢ ((k₁ ≫ biprod.inl + (k₁ ≫ f) ≫ biprod.inr) ≫ biprod.fst) ≫ f ≫ g = 0

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k₁ : A ⟶ X
hk✝ : (k₁ ≫ biprod.inl + (k₁ ≫ f) ≫ biprod.inr) ≫ φ f g = 0
hk : (k₁ ≫ f) ≫ g = 0
⊢ kernel.lift (f ≫ g) ((k₁ ≫ biprod.inl + (k₁ ≫ f) ≫ biprod.inr) ≫ biprod.fst) ⋯ ≫ ι f g =
    k₁ ≫ biprod.inl + (k₁ ≫ f) ≫ biprod.inr

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k₂ : Z ⟶ A
hk : f ≫ g ≫ k₂ = 0
⊢ (f ≫ g) ≫ biprod.inr ≫ (biprod.fst ≫ g ≫ k₂ + biprod.snd ≫ k₂) = 0

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k₂ : Z ⟶ A
hk✝ : φ f g ≫ (biprod.fst ≫ g ≫ k₂ + biprod.snd ≫ k₂) = 0
hk : f ≫ g ≫ k₂ = 0
⊢ π f g ≫ cokernel.desc (f ≫ g) (biprod.inr ≫ (biprod.fst ≫ g ≫ k₂ + biprod.snd ≫ k₂)) ⋯ =
    biprod.fst ≫ g ≫ k₂ + biprod.snd ≫ k₂

Tactic:
aesop

Goal state after:
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
⊢ kernel.map f (f ≫ g) (𝟙 X) g ⋯ ≫ kernel.map (f ≫ g) g f (𝟙 Z) ⋯ = 0

Tactic:
aesop

Goal state after:
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
⊢ cokernel.map f (f ≫ g) (𝟙 X) g ⋯ ≫ cokernel.map (f ≫ g) g f (𝟙 Z) ⋯ = 0

Tactic:
aesop

Goal state after:
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
⊢ (-kernel.ι g) ≫ (snakeInput f g).L₂.f = (kernel.ι g ≫ biprod.inr) ≫ (snakeInput f g).v₁₂.τ₂

Tactic:
aesop

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
ι : Type u_2
inst✝² : HasProductsOfShape ι C
ι' : Type u_3
inst✝¹ : HasProductsOfShape ι' C
inst✝ : IsIPCOfShape.{w, u_2, v_1, u_1} ι C
e : ι ≃ ι'
J : ι' → Type w
x✝¹ : (i : ι') → SmallCategory (J i)
x✝ : ∀ (i : ι'), IsFiltered (J i)
F : (i : ι') → J i ⥤ C
c : (i : ι') → Cocone (F i)
hc : (i : ι') → IsColimit (c i)
h : IsColimit (coconePointwiseProduct fun i ↦ c (e i))
⊢ ((Pi.equivalenceOfEquiv J e).symm.functor ⋙ pointwiseProduct fun i ↦ F (e i)) ≅ pointwiseProduct F

Tactic:
exact (Pi.equivalenceOfEquivCompPointwiseProduct F e)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected

Goal state before:
pp: J : Type w
inst✝⁵ : Category.{w', w} J
inst✝⁴ : IsConnected J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPushouts C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
F : J ⥤ C
c : Cone F
hc : IsLimit c
X Y : C
g h : Y ⟶ c.pt
f : c.pt ⟶ X
hf : ∀ (j : J), g ≫ f ≫ pushout.inr (c.π.app j) f = h ≫ f ≫ pushout.inr (c.π.app j) f
⊢ g ≫ f = h ≫ f

Tactic:
refine (hc.pushoutOfHasExactLimitsOfShape f).hom_ext (fun j => ?_)
  rw [← cancel_mono (pushoutObjIso _ _ _).hom]
  simpa using! hf j

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
f : (preadditiveCoyonedaObj G).obj A ⟶ (preadditiveCoyonedaObj G).obj B
⊢ ∃ a, (preadditiveCoyonedaObj G).map a = f

Tactic:
have := (isSeparator_iff_epi G).1 hG A

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
f : (preadditiveCoyonedaObj G).obj A ⟶ (preadditiveCoyonedaObj G).obj B
this : Epi (Sigma.desc fun f ↦ f)
⊢ ∃ a, (preadditiveCoyonedaObj G).map a = f
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: case g_comm
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
⊢ (injectiveResolution X).ι ≫
      desc f (injectiveResolution Y) (injectiveResolution X) ≫ ((injectiveResolution Y).homotopyEquiv J).hom =
    (CochainComplex.single₀ C).map f ≫ J.ι

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: case h_comm
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
⊢ (injectiveResolution X).ι ≫ ((injectiveResolution X).homotopyEquiv I).hom ≫ φ = (CochainComplex.single₀ C).map f ≫ J.ι

Tactic:
aesop

Goal state after: