mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case pos
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
hf : HasGaussNorm v c f
hg : HasGaussNorm v c g
hfg : HasGaussNorm v c (f * g)
vNonneg : ∀ (a : R), v a ≥ 0
vZero : v 0 = 0
vNA : IsNonarchimedean v
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vNeg : ∀ (a : R), v (-a) = v a
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hdom :
  ∃ i j,
    AchievesGaussNorm v c f i ∧
      AchievesGaussNorm v c g j ∧
        ∀ p ∈ Finset.antidiagonal (i + j),
          p ≠ (i, j) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i) f) * v ((coeff j) g)
hf' : ¬f = 0
hg' : g = 0
⊢ gaussNorm v c (f * g) = gaussNorm v c f * gaussNorm v c g

pp: case neg
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
hf : HasGaussNorm v c f
hg : HasGaussNorm v c g
hfg : HasGaussNorm v c (f * g)
vNonneg : ∀ (a : R), v a ≥ 0
vZero : v 0 = 0
vNA : IsNonarchimedean v
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vNeg : ∀ (a : R), v (-a) = v a
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hdom :
  ∃ i j,
    AchievesGaussNorm v c f i ∧
      AchievesGaussNorm v c g j ∧
        ∀ p ∈ Finset.antidiagonal (i + j),
          p ≠ (i, j) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i) f) * v ((coeff j) g)
hf' : ¬f = 0
hg' : ¬g = 0
⊢ gaussNorm v c (f * g) = gaussNorm v c f * gaussNorm v c g

Tactic:
· simp [hg', gaussNorm_zero v c vZero]

Goal state after:
case neg
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
hf : HasGaussNorm v c f
hg : HasGaussNorm v c g
hfg : HasGaussNorm v c (f * g)
vNonneg : ∀ (a : R), v a ≥ 0
vZero : v 0 = 0
vNA : IsNonarchimedean v
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vNeg : ∀ (a : R), v (-a) = v a
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hdom :
  ∃ i j,
    AchievesGaussNorm v c f i ∧
      AchievesGaussNorm v c g j ∧
        ∀ p ∈ Finset.antidiagonal (i + j),
          p ≠ (i, j) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i) f) * v ((coeff j) g)
hf' : ¬f = 0
hg' : ¬g = 0
⊢ gaussNorm v c (f * g) = gaussNorm v c f * gaussNorm v c g
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ rexp ((2 * π)⁻¹ * ∫ (x : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 x) p‖) ≤
    rexp ((2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, log (p.sum fun x a ↦ ‖a‖))

Tactic:
smul_eq_mul

Goal state after:
case neg
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ rexp ((2 * π)⁻¹ * ∫ (x : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 x) p‖) ≤
    rexp ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, log (p.sum fun x a ↦ ‖a‖))
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg
p : ℂ[X]
this✝¹ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this✝ : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ p.mahlerMeasure ≤ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2)

Tactic:
simp only [mahlerMeasure, logMahlerMeasure, ne_eq, hp, not_false_eq_true, ↓reduceIte]

Goal state after:
case neg
p : ℂ[X]
this✝¹ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this✝ : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ rexp (circleAverage (fun x ↦ log ‖eval x p‖) 0 1) ≤ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2)
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg
p : ℂ[X]
this✝¹ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this✝ : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ rexp (circleAverage (fun x ↦ log ‖eval x p‖) 0 1) ≤ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2)

Tactic:
circleAverage_eq_intervalAverage

Goal state after:
case neg
p : ℂ[X]
this✝¹ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this✝ : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ rexp (⨍ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) ≤ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2)
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
hx : Germ.Tendsto x (𝓝 0)
⊢ ArchimedeanClass.mk x ≠ 0

Tactic:
rw [← stdPart_eq_zero, stdPart_of_tendsto hx]

Goal state after:
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
⊢ x.InfiniteNeg ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0

Tactic:
rw [← infinitePos_neg, infinitePos_iff_infinitesimal_inv_pos, inv_neg, neg_pos, infinitesimal_neg]

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: case hf0
⊢ Tendsto (fun i ↦ (2 * ↑i + 1)⁻¹) atTop (𝓝 0)

Tactic:
apply Tendsto.inv_tendsto_atTop; apply tendsto_atTop_add_const_right
      exact tendsto_natCast_atTop_atTop.const_mul_atTop zero_lt_two

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

Goal state before:
pp: case inr.inl
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
hp₁ : 1 < p
⊢ binEntropy p ≠ 0

Tactic:
exact (binEntropy_neg_of_one_lt hp₁).ne

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

Goal state before:
pp: q : ℕ
⊢ ¬ContinuousAt (deriv (qaryEntropy q)) 0

Tactic:
have tendstoTop : Tendsto (fun p ↦ log (q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop := by
    have : (fun p ↦ log (q - 1) + log (1 - p) - log p)
        = (fun p ↦ log (q - 1) + (log (1 - p) - log p)) := by ext; ring
    rw [this]
    exact tendsto_atTop_add_const_left _ _ tendsto_log_one_sub_sub_log_nhdsGT_atAtop

Goal state after:
q : ℕ
tendstoTop : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
⊢ ¬ContinuousAt (deriv (qaryEntropy q)) 0
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
c ε r : ℝ
hc : c ≠ 0
u : ℝ → E := fun x ↦ x⁻¹ • f x
key : (fun x ↦ x⁻¹ • f (c * x)) = fun x ↦ c • u (c * x)
⊢ ∫ (x : ℝ) in ε..r, x⁻¹ • f (c * x) = ∫ (x : ℝ) in c * ε..c * r, x⁻¹ • f x

Tactic:
rw [key, intervalIntegral.integral_smul, smul_integral_comp_mul_left]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
c ε r : ℝ
hc : c ≠ 0
⊢ ∫ (x : ℝ) in ε..r, x⁻¹ • f (c * x) = ∫ (x : ℝ) in c * ε..c * r, x⁻¹ • f x

Tactic:
let u : ℝ → E := fun x ↦ x⁻¹ • f x
  have key : (fun x ↦ x⁻¹ • f (c * x)) = fun x ↦ c • u (c * x) := by
    funext x
    simp only [u, smul_smul]
    congr 1
    field_simp
  rw [key, intervalIntegral.integral_smul, smul_integral_comp_mul_left]

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

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

Tactic:
simp [rpowIntegrand₀₁, ht', hp.1.ne', hp₂]

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: ⊢ eulerMascheroniSeq' 1 = 1

Tactic:
by
  simp [eulerMascheroniSeq']

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

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

Tactic:
smul_eq_mul

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Digamma

Goal state before:
pp: s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
hs0 : s ≠ 0
⊢ s⁻¹ + s * deriv Gamma s / (s * Gamma s) = deriv Gamma s / Gamma s + s⁻¹

Tactic:
mul_div_mul_left _ _ hs0,

Goal state after:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
hs0 : s ≠ 0
⊢ s⁻¹ + deriv Gamma s / Gamma s = deriv Gamma s / Gamma s + s⁻¹
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 : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r ≤ ↑b ^ clog b r

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 ^ clog b r

Tactic:
· rw [clog_of_right_le_zero _ hr, zpow_zero]
    exact hr.trans zero_le_one

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 ^ clog b r
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hy : 0 < y
⊢ logb b x < logb b y ↔ y < x

Tactic:
rw [logb, logb, div_lt_div_right_of_neg (log_neg b_pos b_lt_one)]
  exact log_lt_log_iff hy hx

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

Goal state before:
pp: b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ logb b x ≤ y ↔ b ^ y ≤ x

Tactic:
by
  rw [← rpow_le_rpow_left_iff_of_base_lt_one b_pos b_lt_one, rpow_logb b_pos (b_ne_one b_lt_one) hx]

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

Goal state before:
pp: E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
f : C(E, ℝ)
hε : 0 < ε
⊢ ∀ (x y : E),
    dist ({ toFun := fun x ↦ ε.mulExpNegMulSq (f x), continuous_toFun := ⋯ }.toFun x)
        ({ toFun := fun x ↦ ε.mulExpNegMulSq (f x), continuous_toFun := ⋯ }.toFun y) ≤
      2 * (√ε)⁻¹

Tactic:
exact fun x y => dist_mulExpNegMulSq_le_two_mul_sqrt hε (f x) (f y)

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

Goal state before:
pp: case inl
n : ℕ
h_eq : n = 0
⊢ ConvexOn ℝ (Set.Ici (↑n - 1)) fun x ↦ Polynomial.eval x (descPochhammer ℝ n)

Tactic:
simp [h_eq, convexOn_const, convex_Ici]

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
μ : Measure E
inst✝ : BorelSpace E
s : Set ↑(sphere 0 1)
hs : MeasurableSet s
⊢ dim E •
      μ (Subtype.val ∘ ⇑(homeomorphUnitSphereProd E).symm '' (Prod.fst ⁻¹' s ∩ univ ×ˢ Iio ⟨1, toSphere._proof_1⟩)) =
    ↑(dim E) * μ (Ioo 0 1 • Subtype.val '' s)

Tactic:
image_comp,

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
s : Set ↑(sphere 0 1)
hs : MeasurableSet s
⊢ dim E •
      μ (Subtype.val '' ⇑(homeomorphUnitSphereProd E).symm '' (Prod.fst ⁻¹' s ∩ univ ×ˢ Iio ⟨1, toSphere._proof_1⟩)) =
    ↑(dim E) * μ (Ioo 0 1 • Subtype.val '' s)
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
habs : |1 - ε / 4| = 1 - ε / 4
hy : dist 0 ((1 - ε / 4) • x) < ε / 4
⊢ 1 - ε / 4 < ε / 4

Tactic:
simpa [norm_smul, habs, hx] using hy

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n a b : ℕ
hn : n ≠ 0
x✝ : a ≤ n.nthRoot b ∨ n.nthRoot b < a
⊢ a ≤ n.nthRoot b ↔ a ^ n ≤ b

Tactic:
cases le_or_gt a (nthRoot n b) with

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

Goal state before:
pp: case hg
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable fun i ↦ if ↑i = ↑l₀ then 1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2 else 0

Tactic:
exact summable_of_hasFiniteSupport ((Set.finite_singleton l₀).subset (by simp))

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

Goal state before:
pp: case hg
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable fun i ↦ if ↑i = ↑l₀ then -2 / (z - ↑l₀) ^ 3 else 0

Tactic:
exact summable_of_hasFiniteSupport ((Set.finite_singleton l₀).subset (by simp))

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

Goal state before:
pp: n : ℕ
this : log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ 1 - 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))

Tactic:
stirlingSeq_one,

Goal state after:
n : ℕ
this : log (rexp 1 / √2) - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ 1 - 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: case hff'
f : ℝ → ℝ
⊢ ∀ x ∈ Ioo (min 1 (-1)) (max 1 (-1)), HasDerivAt arccos (-(1 / √(1 - x ^ 2))) x

Tactic:
exact fun x hx ↦ (hasDerivAt_arccos (by aesop) (by aesop))

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

Goal state before:
pp: n : ℕ
ι : Type u_1
s : Finset ι
P : ι → ℝ[X]
⊢ π / ↑n * ∑ i ∈ range n, eval (cos ((2 * ↑i + 1) / (2 * ↑n) * π)) (∑ i ∈ s, P i) =
    ∑ i ∈ s, π / ↑n * ∑ i_1 ∈ range n, eval (cos ((2 * ↑i_1 + 1) / (2 * ↑n) * π)) (P i)

Tactic:
eval_finsetSum

Goal state after:
n : ℕ
ι : Type u_1
s : Finset ι
P : ι → ℝ[X]
⊢ π / ↑n * ∑ x ∈ range n, ∑ i ∈ s, eval (cos ((2 * ↑x + 1) / (2 * ↑n) * π)) (P i) =
    ∑ i ∈ s, π / ↑n * ∑ i_1 ∈ range n, eval (cos ((2 * ↑i_1 + 1) / (2 * ↑n) * π)) (P i)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
ι : Type u_1
s : Finset ι
P : ι → ℝ[X]
⊢ sumZeroes n (∑ i ∈ s, P i) = ∑ i ∈ s, sumZeroes n (P i)

Tactic:
simp_rw [sumZeroes, eval_finsetSum]
  rw [sum_comm, mul_sum]

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

Goal state before:
pp: n : ℕ
c : ℝ
P : ℝ[X]
⊢ π / ↑n * c • ∑ x ∈ range n, eval (cos ((2 * ↑x + 1) / (2 * ↑n) * π)) P =
    c * (π / ↑n * ∑ x ∈ range n, eval (cos ((2 * ↑x + 1) / (2 * ↑n) * π)) P)

Tactic:
smul_eq_mul

Goal state after:
n : ℕ
c : ℝ
P : ℝ[X]
⊢ π / ↑n * (c * ∑ x ∈ range n, eval (cos ((2 * ↑x + 1) / (2 * ↑n) * π)) P) =
    c * (π / ↑n * ∑ x ∈ range n, eval (cos ((2 * ↑x + 1) / (2 * ↑n) * π)) P)
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
z : ℂ := Complex.exp (↑k / (2 * ↑n) * ↑π * I)
hz : z = Complex.exp (↑k / (2 * ↑n) * ↑π * I)
⊢ Complex.exp (↑k / ↑n * ↑π * I) = z ^ 2

Tactic:
hz,

Goal state after:
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : (-1) ^ (-k) = (-1) ^ k
z : ℂ := Complex.exp (↑k / (2 * ↑n) * ↑π * I)
hz : z = Complex.exp (↑k / (2 * ↑n) * ↑π * I)
⊢ Complex.exp (↑k / ↑n * ↑π * I) = Complex.exp (↑k / (2 * ↑n) * ↑π * I) ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

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

Tactic:
simp_rw [sumZeroes_smul, smul_eq_mul, MeasureTheory.integral_const_mul]
    congr! with i hrange
    simp_rw [chebyshevTsequence]
    by_cases i = 0
    case pos hi => rw [hi, Nat.cast_zero, integral_eval_T_real_measureT_zero, sumZeroes_T_zero hn]
    case neg hi =>
      have : ¬ (2 * n : ℤ) ∣ i := by
        refine (Int.not_dvd_iff_lt_mul_succ _ (by grind)).mpr ⟨0, ⟨by grind, ?_⟩⟩
        rw_mod_cast [zero_add, mul_one]
        exact mem_range.mp hrange
      rw [integral_eval_T_real_measureT_of_ne_zero (by grind), sumZeroes_T_of_not_dvd this]

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

Goal state before:
pp: case e'_5
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
z : ℂ
hz : ‖z‖ < ↑r
this :
  (∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z‖ < ‖↑l - x‖) →
    HasSum (fun i ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i) (℘[L - l₀] (x + z))
A : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ↑r < ‖↑l - x‖
i : ℕ
⊢ (if i = 0 then ℘[L - l₀] x
      else (↑i + 1) * (L.sumInvPow x (i + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (i + 2))⁻¹ else 0)) •
      z ^ i =
    (if i = 0 then ℘[L - l₀] x
      else (↑i + 1) * (L.sumInvPow x (i + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (i + 2))⁻¹ else 0)) *
      z ^ i

Tactic:
smul_eq_mul

Goal state after:
case e'_5
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
z : ℂ
hz : ‖z‖ < ↑r
this :
  (∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z‖ < ‖↑l - x‖) →
    HasSum (fun i ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i) (℘[L - l₀] (x + z))
A : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ↑r < ‖↑l - x‖
i : ℕ
⊢ (if i = 0 then ℘[L - l₀] x
      else (↑i + 1) * (L.sumInvPow x (i + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (i + 2))⁻¹ else 0)) *
      z ^ i =
    (if i = 0 then ℘[L - l₀] x
      else (↑i + 1) * (L.sumInvPow x (i + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (i + 2))⁻¹ else 0)) *
      z ^ i
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
⊢ (T ℝ ↑n).roots = (Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)).val

Tactic:
wlog! hn : n ≠ 0
  · simp [hn]
  refine roots_eq_of_degree_eq_card (fun x hx ↦ ?_) ?_
  · obtain ⟨k, hk, hx⟩ := Finset.mem_image.mp hx
    rw [← hx, T_real_cos, cos_eq_zero_iff]
    use k
    field_simp
    norm_cast
  · rw [Finset.card_image_of_injOn, Finset.card_range, degree_T, Int.natAbs_natCast]
    exact (Finset.range n).nodup_map_iff_injOn.mp (roots_T_real_nodup n)

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

Goal state before:
pp: a b : ℤ
this : ∀ (x : Fin 2 → ℤ), ![x 0 + a, x 1 + b] = x + ![a, b]
⊢ (fun m ↦ ‖![m 0 + a, m 1 + b]‖⁻¹) =Θ[cofinite] fun m ↦ ‖m‖⁻¹

Tactic:
simpa only [isTheta_inv, isTheta_norm_left, this] using! (IsTheta.add_isLittleO
  (by rw [← isTheta_norm_left]) (isLittleO_const_left_of_properSpace_of_discreteTopology ![a, b]))

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

Goal state before:
pp: case mp
n : ℕ
hn : 2 ≤ n
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑(n - 1) + 1))) (Finset.range (n - 1))
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos ((↑k + 1) * π / (↑(n - 1) + 1)) = x
⊢ x = cos (↑(k + 1) * π / ↑n)

Tactic:
← 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 : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos ((↑k + 1) * π / (↑(n - 1) + 1)) = x
⊢ cos ((↑k + 1) * π / (↑(n - 1) + 1)) = cos (↑(k + 1) * π / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case pos
L : PeriodPair
x : ↥L.lattice
this : AnalyticAt ℂ L.relation 0
⊢ AnalyticAt ℂ L.relation ↑x

Tactic:
← sub_self x.1

Goal state after:
case pos
L : PeriodPair
x : ↥L.lattice
this : AnalyticAt ℂ L.relation (↑x - ↑x)
⊢ AnalyticAt ℂ L.relation ↑x
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:
rw [← mul_add_one, fib_two_mul]

Goal state after:
n : ℤ
⊢ fib (n + 1) * (2 * fib (n + 1 + 1) - fib (n + 1)) = fib (n + 1) * (2 * fib n + fib (n + 1))
Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Injective

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
h : (preadditiveYoneda.obj J ⋙ forget AddCommGrpCat).PreservesEpimorphisms
⊢ (preadditiveYoneda.obj J).PreservesEpimorphisms

Tactic:
exact
      Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveYoneda.obj J) (forget _)

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ (ComplexShape.up ℕ).next (n + 1) = n + 2

Tactic:
simp only [CochainComplex.next]; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square

Goal state before:
pp: case refine_3
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₂) = ⇑(ConcreteCategory.hom sq₂.f₁₂) ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₃) = ⇑(ConcreteCategory.hom sq₂.f₁₃) ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₂₄) = ⇑(ConcreteCategory.hom sq₂.f₂₄) ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₃₄) = ⇑(ConcreteCategory.hom sq₂.f₃₄) ∘ ⇑e₃
x✝ : (sq₁.map uliftFunctor.{max u v, v}).X₂
⊢ ((ConcreteCategory.hom
            ((sq₁.map uliftFunctor.{max u v, v}).f₂₄ ≫ ((Equiv.ulift.trans e₄).trans Equiv.ulift.symm).toIso.hom)).toFun
        x✝).down =
    ((ConcreteCategory.hom
            (((Equiv.ulift.trans e₂).trans Equiv.ulift.symm).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₂₄)).toFun
        x✝).down

Tactic:
simpa [types_comp, uliftFunctor_map] using congrFun comm₂₄ _

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
p : ℕ
hp : p + 1 = n
⊢ R.extMk f m hm hf = 0 ↔ ∃ g, g ≫ R.cocomplex.d p n = f

Tactic:
simp only [← R.extEquivCohomologyClass.apply_eq_iff_eq,
    extEquivCohomologyClass_extMk, extEquivCohomologyClass_zero,
    CohomologyClass.mk_eq_zero_iff]
  rw [Cocycle.fromSingleMk_mem_coboundaries_iff _ _ _ _ _ p (by lia),
    R.cochainComplex_d _ _ _ _ rfl rfl]
  exact ⟨fun ⟨g, hg⟩ ↦ ⟨g ≫ (R.cochainComplexXIso p p rfl).hom,
      by simp only [← cancel_mono (R.cochainComplexXIso n n rfl).inv, Category.assoc, hg]⟩,
    fun ⟨g, hg⟩ ↦ ⟨g ≫ (R.cochainComplexXIso p p rfl).inv, by simp [← hg]⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
⊢ Function.Injective (pseudoApply f)

Tactic:
intro abar abar'

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
⊢ pseudoApply f abar = pseudoApply f abar' → abar = abar'