mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: case hflt
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
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ ∀ᵐ (x : ↑(Ioi 0)) ∂Measure.comap Subtype.val volume, ENNReal.ofReal (↑x ^ (dim E - 1)) < ∞

Tactic:
simp

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

Goal state before:
pp: L : PeriodPair
l : ℂ
⊢ l ∈ (↑L.lattice \ {l})ᶜ

Tactic:
simp

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

Goal state before:
pp: case neg
a b : Multiset ℂ
h : a.card = b.card + 1
j : ℂ
hj : j ∈ a
k : ℕ
h' : j = -↑k
⊢ 1 ≤ ⊤

Tactic:
simp

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

Goal state before:
pp: ⊢ (fun z ↦ (regularizedHGFunSeries 0 0).sum z) = (NormedSpace.expSeries ℂ ℂ).sum

Tactic:
simp

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ 1 < Module.rank ℝ ℂ

Tactic:
simp

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

Goal state before:
pp: b c : ℂ
k : ℕ
⊢ -↑k ∈ {-↑k, b}

Tactic:
simp

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

Goal state before:
pp: a c : ℂ
k : ℕ
⊢ -↑k ∈ {a, -↑k}

Tactic:
simp

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

Goal state before:
pp: a b c : ℂ
h : ∀ (k : ℕ), a ≠ -↑k ∧ b ≠ -↑k
⊢ ∀ j ∈ {a, b}, ∀ (k : ℕ), j ≠ -↑k

Tactic:
simp

Goal state after:
a b c : ℂ
h : ∀ (k : ℕ), a ≠ -↑k ∧ b ≠ -↑k
⊢ (∀ (k : ℕ), ¬a = -↑k) ∧ ∀ (k : ℕ), ¬b = -↑k
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
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ μ.toSphere ≠ 0

Tactic:
simp

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ DifferentiableOn ℂ (fun x ↦ 1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2) (↑L.lattice \ {l₀ - ↑l})ᶜ

Tactic:
simp

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

Goal state before:
pp: x✝ : { x // x ∈ I }
⊢ x✝ ∈ Subtype.val ⁻¹' Ioo 0 1 ↔ x✝ ∈ Ioo 0 1

Tactic:
simp

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

Goal state before:
pp: L : PeriodPair
z : ℂ
hl : ↑0 / 2 ∉ L.lattice
⊢ False

Tactic:
simp at hl

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

Goal state before:
pp: L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∈ L.lattice
⊢ z ∈ (↑L.lattice \ {z + ↑l - ↑l})ᶜ

Tactic:
simp

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

Goal state before:
pp: case pos
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∈ L.lattice
this : ℘[L - z + ↑l] (z + ↑l) = ℘[L - z + ↑l - ↑l] z + (1 / (z + ↑l) ^ 2 - 1 / (z + ↑l - ↑l) ^ 2)
⊢ ℘[L - z + ↑l - ↑l] z + (1 / (z + ↑l) ^ 2 - 1 / (z + ↑l - ↑l) ^ 2) +
      (1 / (z + ↑l - ↑⟨z + ↑l, ⋯⟩) ^ 2 - 1 / ↑⟨z + ↑l, ⋯⟩ ^ 2) =
    ℘[L - ↑⟨z, hz⟩] z + (1 / (z - ↑⟨z, hz⟩) ^ 2 - 1 / ↑⟨z, hz⟩ ^ 2)

Tactic:
simp

Goal state after:
case pos
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∈ L.lattice
this : ℘[L - z + ↑l] (z + ↑l) = ℘[L - z + ↑l - ↑l] z + (1 / (z + ↑l) ^ 2 - 1 / (z + ↑l - ↑l) ^ 2)
⊢ ℘[L - z] z + (((z + ↑l) ^ 2)⁻¹ - (z ^ 2)⁻¹) + -((z + ↑l) ^ 2)⁻¹ = ℘[L - z] z + -(z ^ 2)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: case zero
θ : ℂ
⊢ eval (cos θ) (T ℂ 0) = cos (↑0 * θ)

Tactic:
simp

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

Goal state before:
pp: case one
θ : ℂ
⊢ eval (cos θ) (T ℂ 1) = cos (↑1 * θ)

Tactic:
simp

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

Goal state before:
pp: case neg
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∉ L.lattice
this : ℘[L - 0] (z + ↑l) = ℘[L - -↑l] z + -(↑l ^ 2)⁻¹
⊢ ℘[L - -↑l] z + -(↑l ^ 2)⁻¹ + (1 / (z + ↑l - 0) ^ 2 - 1 / 0 ^ 2) =
    ℘[L - ↑(-l)] z + (1 / (z - ↑(-l)) ^ 2 - 1 / ↑(-l) ^ 2)

Tactic:
simp

Goal state after:
case neg
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∉ L.lattice
this : ℘[L - 0] (z + ↑l) = ℘[L - -↑l] z + -(↑l ^ 2)⁻¹
⊢ ℘[L - -↑l] z + -(↑l ^ 2)⁻¹ + ((z + ↑l) ^ 2)⁻¹ = ℘[L - -↑l] z + (((z + ↑l) ^ 2)⁻¹ - (↑l ^ 2)⁻¹)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: case zero
θ : ℂ
⊢ eval (cos θ) (U ℂ 0) * sin θ = sin ((↑0 + 1) * θ)

Tactic:
simp

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

Goal state before:
pp: L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ 0 ∈ {z | (fun x ↦ ℘[L] (x + z)) = ℘[L]}

Tactic:
simp

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

Goal state before:
pp: L : PeriodPair
z✝ : ℂ
l : ↥L.lattice
z : ℂ
hz : z ∈ {z | (fun x ↦ ℘[L] (x + z)) = ℘[L]}
i : ℂ
| (fun x ↦ ℘[L] (x + z)) (i + -z)

Tactic:
simp

Goal state after:
L : PeriodPair
z✝ : ℂ
l : ↥L.lattice
z : ℂ
hz : z ∈ {z | (fun x ↦ ℘[L] (x + z)) = ℘[L]}
i : ℂ
| ℘[L] i
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ ℘[L] (z + ↑l) = ℘[L] z

Tactic:
by
  let G : AddSubgroup ℂ :=
    { carrier := { z | (℘[L] <| · + z) = ℘[L] }
      add_mem' := by simp_all [funext_iff, ← add_assoc]
      zero_mem' := by simp
      neg_mem' {z} hz := funext fun i ↦ by conv_lhs => rw [← hz]; simp }
  have : L.lattice ≤ G.toIntSubmodule := by
    rw [lattice, Submodule.span_le]
    rintro _ (rfl | rfl)
    · ext i
      exact L.weierstrassP_add_coe_aux _ ⟨_, L.ω₁_mem_lattice⟩ L.ω₁_div_two_notMem_lattice
    · ext i
      exact L.weierstrassP_add_coe_aux _ ⟨_, L.ω₂_mem_lattice⟩ L.ω₂_div_two_notMem_lattice
  exact congr_fun (this l.2) _

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

Goal state before:
pp: L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ (Function.support fun i ↦ if ↑i = ↑l₀ then -2 / (z - ↑l₀) ^ 3 else 0) ⊆ {l₀}

Tactic:
simp

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

Goal state before:
pp: h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
this : sin ∘ arcsin =ᶠ[𝓝[≥] (-1)] id
⊢ id (-1) = sin (arcsin (-1))

Tactic:
simp

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

Goal state before:
pp: case neg.inl
⊢ 0 = 1 / √(1 - (-1) ^ 2)

Tactic:
simp

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

Goal state before:
pp: case neg.inr
⊢ 0 = 1 / √(1 - 1 ^ 2)

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: case inl
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a a)
hab : a ≤ a
⊢ ∫ (x : ℝ) in a..a, deriv f x = f a - f a

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ log (stirlingSeq 0) = log ↑0! - 1 / 2 * log (2 * ↑0) - ↑0 * log (↑0 / rexp 1)

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
⊢ 0 + 1 ≤ 1

Tactic:
simp

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

Goal state before:
pp: L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ (Function.support fun l ↦ if l = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3)) else 0) ⊆ {⟨l₀, hl₀⟩}

Tactic:
simp

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

Goal state before:
pp: n : ℕ
f : ℕ → ℝ := fun k ↦ log (stirlingSeq (k + 1))
g : ℕ → ℝ := fun k ↦ 1 / (12 * (↑k + 1))
hf : log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 1 / (12 * (↑0 + 1)) - 1 / (12 * (↑n + 1))
⊢ log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 12⁻¹

Tactic:
hf

Goal state after:
n : ℕ
f : ℕ → ℝ := fun k ↦ log (stirlingSeq (k + 1))
g : ℕ → ℝ := fun k ↦ 1 / (12 * (↑k + 1))
hf : log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 1 / (12 * (↑0 + 1)) - 1 / (12 * (↑n + 1))
⊢ 1 / (12 * (↑0 + 1)) - 1 / (12 * (↑n + 1)) ≤ 12⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
f : ℕ → ℝ := fun k ↦ log (stirlingSeq (k + 1))
g : ℕ → ℝ := fun k ↦ 1 / (12 * (↑k + 1))
hf : log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 1 / (12 * (↑0 + 1)) - 1 / (12 * (↑n + 1))
⊢ 1 / (12 * (↑0 + 1)) - 1 / (12 * (↑n + 1)) ≤ 12⁻¹

Tactic:
simp

Goal state after:
n : ℕ
f : ℕ → ℝ := fun k ↦ log (stirlingSeq (k + 1))
g : ℕ → ℝ := fun k ↦ 1 / (12 * (↑k + 1))
hf : log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 1 / (12 * (↑0 + 1)) - 1 / (12 * (↑n + 1))
⊢ 0 ≤ ↑n + 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: ⊢ ∀ x ∈ Set.Ioo (min (-1) 1) (max (-1) 1), 0 ≤ √(1 - x ^ 2)⁻¹

Tactic:
simp

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

Goal state before:
pp: f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this : IntegrableOn (fun x ↦ f x * √(1 - x ^ 2)⁻¹) (Set.Ioc (-1) 1) volume
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict (Set.Ioc (-1) 1), ↑(NNReal.mk √(1 - x ^ 2)⁻¹ ⋯) < ⊤

Tactic:
simp

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

Goal state before:
pp: f : ℝ → ℝ
⊢ ∫ (x : ℝ) in 1..-1, -(f x * √(1 - x ^ 2)⁻¹) = ∫ (x : ℝ) in 1..-1, f x * -√(1 - x ^ 2)⁻¹

Tactic:
simp

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

Goal state before:
pp: a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
⊢ 2 < 4

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case inl
⊢ √(2 * π * ↑0) * (↑0 / rexp 1) ^ 0 ≤ ↑0!

Tactic:
simp

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

Goal state before:
pp: f : ℝ → ℝ
⊢ ∫ (θ : ℝ) in arccos 1..arccos (-1), f (cos θ) = ∫ (θ : ℝ) in 0..π, f (cos θ)

Tactic:
simp

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

Goal state before:
pp: ⊢ ∫ (θ : ℝ) in 0..π, eval (cos θ) (T ℝ 0) = π

Tactic:
simp

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

Goal state before:
pp: n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
h✝ : 0 ≤ n
⊢ ∫ (θ : ℝ) in 0..↑n * π, deriv sin θ = 0

Tactic:
integral_deriv_of_contDiffOn_Icc contDiff_sin.contDiffOn (by positivity)

Goal state after:
n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
h✝ : 0 ≤ n
⊢ sin (↑n * π) - sin 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
h✝ : 0 ≤ n
⊢ sin (↑n * π) - sin 0 = 0

Tactic:
simp

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

Goal state before:
pp: n : ℤ
hn✝ : n ≠ 0
hn' : ↑n ≠ 0
hn : n < 0
⊢ -(sin 0 - sin (↑n * π)) = 0

Tactic:
simp

Goal state after:
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κ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
⊢ -3 < -↑(finrank ℤ ↥L.lattice)

Tactic:
simp

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

Goal state before:
pp: n m : ℕ
h : n ≠ m
⊢ (0 + 0) / 2 = 0

Tactic:
simp

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

Goal state before:
pp: ⊢ T ℝ 0 * T ℝ 0 = T ℝ 0

Tactic:
simp

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

Goal state before:
pp: case inl
⊢ StrictAntiOn (fun x ↦ node 0 x) ↑(Finset.range (0 + 1))

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ (algebraMap ℤ ℂ) ↑2 ∈ nonZeroDivisors ℂ

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ (algebraMap ℤ ℝ) ↑2 ∈ nonZeroDivisors ℝ

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case «0»
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hk : 2 * cos (↑r * π) = ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 0)
⊢ ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 0) / 2 ∈ {-1, -1 / 2, 0, 1 / 2, 1}

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case «1»
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hk : 2 * cos (↑r * π) = ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 1)
⊢ ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 1) / 2 ∈ {-1, -1 / 2, 0, 1 / 2, 1}

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case «2»
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hk : 2 * cos (↑r * π) = ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 2)
⊢ ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 2) / 2 ∈ {-1, -1 / 2, 0, 1 / 2, 1}

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case «3»
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hk : 2 * cos (↑r * π) = ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 3)
⊢ ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 3) / 2 ∈ {-1, -1 / 2, 0, 1 / 2, 1}

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case «4»
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hk : 2 * cos (↑r * π) = ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 4)
⊢ ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 4) / 2 ∈ {-1, -1 / 2, 0, 1 / 2, 1}

Tactic:
simp

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
hmem : P ∈ degreeLT ℝ (2 * n)
⊢ ∀ i < 2 * n, IsUnit (↑(chebyshevTsequence ℝ) i).leadingCoeff

Tactic:
simp

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
hmem : P ∈ Submodule.span ℝ (↑(chebyshevTsequence ℝ) '' Set.Iio (2 * n))
⊢ Set.Iio (2 * n) = ↑(range (2 * n))

Tactic:
simp

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

Goal state before:
pp: case neg.inl
L : PeriodPair
l₀ z : ℂ
κ : ℝ
hκ : 1 < κ
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
p : ℕ × ↥L.lattice
hp :
  ¬↑((Equiv.prodCongrLeft fun x ↦
              { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
            (Prod.map some id p)).2 =
      l₀
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - z‖ < ‖↑l - z‖
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - z‖ * κ < ‖↑l - z‖
H₂ : Summable fun l ↦ ‖↑l - z‖ ^ (-3) * ‖z - z‖
hpx : ‖↑p.2 - z‖ ≠ 0
⊢ ‖((↑((Equiv.prodCongrLeft fun x ↦
                      { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                        right_inv := ⋯ })
                    (Prod.map some id p)).1 +
              1) *
            (↑((Equiv.prodCongrLeft fun x ↦
                        { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                          right_inv := ⋯ })
                      (Prod.map some id p)).2 -
                z) ^
              (-(↑((Equiv.prodCongrLeft fun x ↦
                          { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                            right_inv := ⋯ })
                        (Prod.map some id p)).1 +
                  2)) -
          Nat.rec
            (↑((Equiv.prodCongrLeft fun x ↦
                      { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                        right_inv := ⋯ })
                    (Prod.map some id p)).2 ^
              (-2))
            (fun n n_ih ↦ 0)
            ((Equiv.prodCongrLeft fun x ↦
                  { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
                (Prod.map some id p)).1) *
        (z - z) ^
          ((Equiv.prodCongrLeft fun x ↦
                { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
              (Prod.map some id p)).1‖ ≤
    (↑p.1 + 2) * κ ^ (-↑p.1) * (‖↑p.2 - z‖ ^ (-3) * ‖z - z‖)

Tactic:
simp

Goal state after:
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κ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp :
  ¬↑((Equiv.prodCongrLeft fun x ↦
              { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
            (Prod.map some id p)).2 =
      l₀
hpx : ‖↑p.2 - x‖ ≠ 0
hxz : z ≠ x
⊢ True ∨ -x + z = 0

Tactic:
simp

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

Goal state before:
pp: n : ℕ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ n < n + 1

Tactic:
simp

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

Goal state before:
pp: case e'_3.e'_4
n : ℕ
P : ℝ[X]
hP : P.degree ≤ ↑n
this : P.degree < ↑(Finset.range (n + 1)).card
⊢ n = (Finset.range (n + 1)).card - 1

Tactic:
simp

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

Goal state before:
pp: case pos
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
l : ↥L.lattice
h : ↑l = l₀
⊢ 0 = ∑' (i : ℕ), 0

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ (T ℝ ↑n).degree ≤ ↑n

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ (T ℝ ↑n).leadingCoeff = 2 ^ (n - 1)

Tactic:
simp

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

Goal state before:
pp: case e'_3
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
i : ℕ
⊢ ‖L.weierstrassPExceptSeries l₀ x i‖ * ↑r ^ i =
    ((fun a ↦ ‖a‖) ∘ fun i ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * (x + ↑↑r - x) ^ i) i

Tactic:
simp

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₀})ᶜ
⊢ 0 = ‖0‖

Tactic:
simp

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

Goal state before:
pp: n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ n < n + 1

Tactic:
simp

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
⊢ l₀ ∈ (↑L.lattice \ {l₀})ᶜ

Tactic:
simp

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

Goal state before:
pp: L : PeriodPair
l : ℂ
n : ℕ
⊢ ↑n ! ≠ 0

Tactic:
simp

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

Goal state before:
pp: n : ℤ
x : ℝ
hx : x ≤ -1
⊢ (-1 * -1) ^ n * eval (-x) (T ℝ n) = eval (-x) (T ℝ n)

Tactic:
simp

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

Goal state before:
pp: n : ℤ
hn : n ≠ 0
x : ℝ
hx : x < -1
⊢ (-1 * -1) ^ n * eval (-x) (T ℝ n) = eval (-x) (T ℝ n)

Tactic:
simp

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

Goal state before:
pp: n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
h✝ : ¬(1 ≤ i ∧ i ≤ n - k)
⊢ 0 ∉ Finset.Icc 1 (n - k)

Tactic:
simp

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

Goal state before:
pp: n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
h✝ : 1 ≤ i ∧ i ≤ n - k
⊢ 0 ∉ (Finset.Icc 1 (n - k + 1)).erase i

Tactic:
simp

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

Goal state before:
pp: L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ x ∈ (↑L.lattice \ {x})ᶜ

Tactic:
simp

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ l₀ ∈ (↑L.lattice \ {l₀})ᶜ

Tactic:
simp

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

Goal state before:
pp: case refine_2
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ (fun z ↦ (z - l₀) ^ 2 * ℘[L - l₀] z + 1 - (z - l₀) ^ 2 / l₀ ^ 2) l₀ ≠ 0

Tactic:
simp

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

Goal state before:
pp: L : PeriodPair
this : Meromorphic fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃
z w : ℂ
⊢ w ∈ {z}ᶜ → w ∈ (↑L.lattice \ {z})ᶜ → ℘'[L] w ^ 2 - 4 * ℘[L] w ^ 3 + L.g₂ * ℘[L] w + L.g₃ = L.relation w

Tactic:
hw

Goal state after:
L : PeriodPair
this : Meromorphic fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃
z w : ℂ
hw : w ∈ {z}ᶜ
⊢ w ∈ (↑L.lattice \ {z})ᶜ → ℘'[L] w ^ 2 - 4 * ℘[L] w ^ 3 + L.g₂ * ℘[L] w + L.g₃ = L.relation w
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n k : ℕ
hk : k < n
⊢ (Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)).val.Nodup

Tactic:
simp

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

Goal state before:
pp: case neg
L : PeriodPair
z : ℂ
hz0 : ¬z = 0
hz : z ∉ L.lattice
⊢ (℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃) * id z ^ 6 =
    ((℘'[L] z + 2 / (z - ↑0) ^ 3) * z ^ 3 - 2) ^ 2 - 4 * ((℘[L] z + (1 / ↑0 ^ 2 - 1 / (z - ↑0) ^ 2)) * z ^ 2 + 1) ^ 3 +
        L.g₂ * ((℘[L] z + (1 / ↑0 ^ 2 - 1 / (z - ↑0) ^ 2)) * z ^ 6 + z ^ 4) +
      L.g₃ * z ^ 6

Tactic:
simp

Goal state after:
case neg
L : PeriodPair
z : ℂ
hz0 : ¬z = 0
hz : z ∉ L.lattice
⊢ (℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃) * z ^ 6 =
    ((℘'[L] z + 2 / z ^ 3) * z ^ 3 - 2) ^ 2 - 4 * ((℘[L] z + -(z ^ 2)⁻¹) * z ^ 2 + 1) ^ 3 +
        L.g₂ * ((℘[L] z + -(z ^ 2)⁻¹) * z ^ 6 + z ^ 4) +
      L.g₃ * z ^ 6