mathlib-initiative/mathlib-tactics huggingface dataset:
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 < ε
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε

Tactic:
let := upgradeIsCompletelyPseudoMetrizable α
  cases isEmpty_or_nonempty α
  case inl =>
    refine ⟨∅, by simp, ?_⟩
    rwa [Set.eq_empty_of_isEmpty ∅ᶜ, measure_empty]
  case inr =>
    let seq := TopologicalSpace.denseSeq α
    have hseq_dense : DenseRange seq := TopologicalSpace.denseRange_denseSeq α
    obtain ⟨t : ℕ → SetRel α α,
        ht : ∀ i, t i ∈ 𝓤 α ∧ IsOpen (t i) ∧ (t i).IsSymm,
        h_basis : (uniformity α).HasAntitoneBasis t⟩ :=
      (@uniformity_hasBasis_open_symmetric α _).exists_antitone_subbasis
    choose htu hto _ using ht
    let f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
    have h_univ n : (⋃ m, f n m) = univ := hseq_dense.iUnion_uniformity_ball (htu n)
    have h3 n (ε : ℝ≥0∞) (hε : 0 < ε) : ∃ m, P (⋂ m' ≤ m, (f n m')ᶜ) < ε := by
      refine exists_measure_iInter_lt (fun m ↦ ?_) hε ⟨0, measure_ne_top P _⟩ ?_
      · exact (measurable_prodMk_left (hto n).measurableSet).compl.nullMeasurableSet
      · rw [← compl_iUnion, h_univ, compl_univ]
    choose! s' s'bound using h3
    rcases ENNReal.exists_pos_sum_of_countable' (ne_of_gt hε) ℕ with ⟨δ, hδ1, hδ2⟩
    let u : ℕ → ℕ := fun n ↦ s' n (δ n)
    refine ⟨interUnionBalls seq u t, isCompact_closure_interUnionBalls h_basis.toHasBasis seq u, ?_⟩
    rw [interUnionBalls, Set.compl_iInter]
    refine ((measure_iUnion_le _).trans ?_).trans_lt hδ2
    refine ENNReal.tsum_le_tsum (fun n ↦ ?_)
    have h'' n : Prod.swap ⁻¹' t n = t n := by ext; exact (t n).comm
    simp only [h'', compl_iUnion, ge_iff_le]
    exact (s'bound n (δ n) (hδ1 n)).le

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 < ε
⊢ Continuous[inst✝³, _] fun x ↦ ε.mulExpNegMulSq (f x)

Tactic:
fun_prop

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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < ↑(Module.finrank ℝ E)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
hint : IntegrableOn (fun y ↦ y ^ (Module.finrank ℝ E - 1) • (C * y ^ (-α))) (Ioo 0 r) volume
⊢ IntegrableOn f (ball 0 r) μ

Tactic:
← integrableOn_fun_norm_addHaar μ

Goal state after:
E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < ↑(Module.finrank ℝ E)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
hint : IntegrableOn (fun x ↦ C * ‖x‖ ^ (-α)) (ball 0 r) μ
⊢ IntegrableOn f (ball 0 r) μ
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case hab
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ ‖l‖ / 2 ≤ ‖s - l‖

Tactic:
norm_sub_rev

Goal state after:
case hab
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ ‖l‖ / 2 ≤ ‖l - s‖
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h✝ : ¬↑i = l₀
⊢ DifferentiableOn ℂ (fun z ↦ 1) (↑L.lattice \ {l₀})ᶜ

Tactic:
fun_prop

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h✝ : ¬↑i = l₀
⊢ DifferentiableOn ℂ (fun z ↦ (z - ↑i) ^ 2) (↑L.lattice \ {l₀})ᶜ

Tactic:
fun_prop

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h✝ : ¬↑i = l₀
⊢ DifferentiableOn ℂ (fun z ↦ 1 / ↑i ^ 2) (↑L.lattice \ {l₀})ᶜ

Tactic:
fun_prop

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

Goal state before:
pp: case neg
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 2 * ‖l‖ ^ 3 ≤ 16 * ‖s - ↑l‖ ^ 3

pp: case neg.hb
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 0 < ‖s - ↑l‖ ^ 3

pp: case neg.hd
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 0 < ‖l‖ ^ 3

Tactic:
norm_sub_rev

Goal state after:
case neg
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 2 * ‖l‖ ^ 3 ≤ 16 * ‖↑l - s‖ ^ 3

case neg.hb
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 0 < ‖s - ↑l‖ ^ 3

case neg.hd
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 0 < ‖l‖ ^ 3
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 2 / ‖s - ↑l‖ ^ 3 ≤ 16 * ‖l‖ ^ (-3)

Tactic:
rw [Real.rpow_neg (by positivity), ← div_eq_mul_inv, div_le_div_iff₀, norm_sub_rev]

Goal state after:
case neg
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 2 * ‖l‖ ^ 3 ≤ 16 * ‖↑l - s‖ ^ 3

case neg.hb
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 0 < ‖s - ↑l‖ ^ 3

case neg.hd
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 0 < ‖l‖ ^ 3
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h✝ : ¬↑i = l₀
⊢ DifferentiableOn ℂ (fun z ↦ -2) (↑L.lattice \ {l₀})ᶜ

Tactic:
fun_prop

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h✝ : ¬↑i = l₀
⊢ DifferentiableOn ℂ (fun z ↦ (z - ↑i) ^ 3) (↑L.lattice \ {l₀})ᶜ

Tactic:
fun_prop

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

Goal state before:
pp: a b : Multiset ℂ
⊢ Tendsto
    (fun n ↦ (Multiset.map (fun x ↦ x / ↑n + 1) a).prod / ((Multiset.map (fun x ↦ x / ↑n + 1) b).prod * (1 + (↑n)⁻¹)))
    atTop (𝓝 1)

Tactic:
have h : Tendsto (fun n : ℕ ↦ (n : ℂ)⁻¹) atTop (𝓝 0) := tendsto_inv_atTop_nhds_zero_nat

Goal state after:
a b : Multiset ℂ
h : Tendsto (fun n ↦ (↑n)⁻¹) atTop (𝓝 0)
⊢ Tendsto
    (fun n ↦ (Multiset.map (fun x ↦ x / ↑n + 1) a).prod / ((Multiset.map (fun x ↦ x / ↑n + 1) b).prod * (1 + (↑n)⁻¹)))
    atTop (𝓝 1)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ DifferentiableAt ℂ (fun i ↦ 1) l

Tactic:
fun_prop

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ DifferentiableAt ℂ (fun i ↦ (i - ↑x) ^ 2) l

Tactic:
fun_prop

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ DifferentiableAt ℂ (fun x2 ↦ 1 / ↑x ^ 2) l

Tactic:
fun_prop

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: case hf
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)))
⊢ Measurable fun r ↦ ENNReal.ofReal (↑r ^ (dim E - 1))

Tactic:
fun_prop

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hxs : x ∈ s
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ DifferentiableAt ℂ (fun x2 ↦ 1) l

Tactic:
fun_prop

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hxs : x ∈ s
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ DifferentiableAt ℂ (fun x2 ↦ (x2 - ↑x) ^ 2) l

Tactic:
fun_prop

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hxs : x ∈ s
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ DifferentiableAt ℂ (fun x2 ↦ 1 / ↑x ^ 2) l

Tactic:
fun_prop

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

Goal state before:
pp: a b c : ℂ
⊢ regularizedHGFunSeries {a, b} {c} = regularizedHGFunSeries {b, a} {c}

Tactic:
Multiset.pair_comm

Goal state after:
a b c : ℂ
⊢ regularizedHGFunSeries {b, a} {c} = regularizedHGFunSeries {b, a} {c}
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 ↦ x + ↑l) (↑L.lattice \ {l₀ - ↑l})ᶜ

Tactic:
fun_prop

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : StandardBorelSpace α
inst✝¹ : Infinite α
inst✝ : Countable α
this : PolishSpace ↑(range Nat.cast)
⊢ Nonempty (α ≃ᵐ ↑(range Nat.cast))

Tactic:
refine ⟨PolishSpace.Equiv.measurableEquiv ?_⟩

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : StandardBorelSpace α
inst✝¹ : Infinite α
inst✝ : Countable α
this : PolishSpace ↑(range Nat.cast)
⊢ α ≃ ↑(range Nat.cast)
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: x : ℝ
⊢ AnalyticAt ℝ (fun i ↦ 1 + rexp (-i)) x

Tactic:
fun_prop

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

Goal state before:
pp: ⊢ Differentiable ℝ sigmoid

Tactic:
fun_prop

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

Goal state before:
pp: case a
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
x : ℂ
hx : x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ
⊢ x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ

pp: case a
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
x : ℂ
hx : x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ
⊢ x + ↑l ∈ (↑L.lattice \ {l₀})ᶜ

Tactic:
· simpa using hx

Goal state after:
case a
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
x : ℂ
hx : x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ
⊢ x + ↑l ∈ (↑L.lattice \ {l₀})ᶜ
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

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

Tactic:
congr with w; split_ifs <;> simp only [zero_add, add_zero, *, neg_div]

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 b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f [[a, b]]
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a

Tactic:
simp only [uIcc_of_le hab] at h

Goal state after:
case inl
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hab : a ≤ b
h : ContDiffOn ℝ 1 f (Icc a b)
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: f : ℝ → ℝ
⊢ Measurable fun x ↦ NNReal.mk √(1 - x ^ 2)⁻¹ ⋯

Tactic:
fun_prop

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

Goal state before:
pp: ⊢ IntervalIntegrable (fun x ↦ √(1 - x ^ 2)⁻¹) volume (-1) 1

Tactic:
intervalIntegrable_iff

Goal state after:
⊢ IntegrableOn (fun x ↦ √(1 - x ^ 2)⁻¹) (Set.uIoc (-1) 1) volume
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
⊢ Measurable fun x ↦ ↑(NNReal.mk √(1 - x ^ 2)⁻¹ ⋯)

Tactic:
fun_prop

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

Goal state before:
pp: case hf
f : ℝ → ℝ
⊢ ContinuousOn arccos (uIcc 1 (-1))

Tactic:
fun_prop

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

Goal state before:
pp: n m : ℤ
⊢ ContinuousOn (fun x ↦ eval x (T ℝ (n + m))) (Set.Icc (-1) 1)

Tactic:
fun_prop

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

Goal state before:
pp: n m : ℤ
⊢ ContinuousOn (fun x ↦ eval x (T ℝ (n - m))) (Set.Icc (-1) 1)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
⊢ ∃ q, 2 * cos (↑r * π) = ↑q

Tactic:
exact ⟨2 * hcos.choose, by push_cast; linarith [hcos.choose_spec]⟩

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

Goal state before:
pp: case hab
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 := ⋯
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
⊢ κ ≤ ‖↑p.2 - x‖ / ‖z - x‖

Tactic:
· exact (le_div_iff₀ (by simpa [sub_eq_zero])).mpr ((mul_comm _ _).trans_le (hκ' p.2 hp).le)

Goal state after:
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 : ℕ
hi : i ∈ range (2 * n)
⊢ ContinuousOn (fun x ↦ eval x (c i • ↑(chebyshevTsequence ℝ) i)) (Set.Icc (-1) 1)

Tactic:
fun_prop

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

Goal state before:
pp: case eval_fg
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
x : ℝ
hx : x ∈ Finset.image (fun x ↦ node n x) (Finset.range (n + 1))
hPx : eval x P ≠ eval x (T ℝ ↑n)
i : ℕ
hix : node n i = x
hi : i ∈ Finset.Iic n
h_le :
  ∀ {i : ℕ},
    i ∈ Finset.Iic n →
      (-1) ^ i * eval (node n i) P * ((-1) ^ i * c i) ≤ (-1) ^ i * eval (node n i) (T ℝ ↑n) * ((-1) ^ i * c i)
⊢ ∑ i ≤ n, (-1) ^ i * eval (node n i) P * ((-1) ^ i * c i) <
    ∑ i ≤ n, (-1) ^ i * eval (node n i) (T ℝ ↑n) * ((-1) ^ i * c i)

Tactic:
refine Finset.sum_lt_sum (fun i hi => h_le hi) ⟨i, hi, lt_of_le_of_ne (h_le hi) ?_⟩

Goal state after:
case eval_fg
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
x : ℝ
hx : x ∈ Finset.image (fun x ↦ node n x) (Finset.range (n + 1))
hPx : eval x P ≠ eval x (T ℝ ↑n)
i : ℕ
hix : node n i = x
hi : i ∈ Finset.Iic n
h_le :
  ∀ {i : ℕ},
    i ∈ Finset.Iic n →
      (-1) ^ i * eval (node n i) P * ((-1) ^ i * c i) ≤ (-1) ^ i * eval (node n i) (T ℝ ↑n) * ((-1) ^ i * c i)
⊢ (-1) ^ i * eval (node n i) P * ((-1) ^ i * c i) ≠ (-1) ^ i * eval (node n i) (T ℝ ↑n) * ((-1) ^ i * c i)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mpr
n : ℕ
hn : n ≠ 0
k : ℕ
hk : k ≤ n
⊢ ∃ k_1, ↑k_1 * π = ↑↑n * (↑k * π / ↑n)

Tactic:
exact ⟨k, by simp [field]⟩

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

Goal state before:
pp: case pos
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
this : MeromorphicAt ℘[L - x] x
⊢ MeromorphicAt (fun x_1 ↦ ℘[L - x] x_1 + (1 / (x_1 - x) ^ 2 - 1 / x ^ 2)) x

Tactic:
fun_prop

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

Goal state before:
pp: L : PeriodPair
⊢ Meromorphic (deriv ℘[L])

Tactic:
fun_prop

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

Goal state before:
pp: case pos
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
h : -k = 0
⊢ 0 ^ (-k) ≤ r z ^ (-k) * 0 ^ (-k)

pp: case neg
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
h : ¬-k = 0
⊢ 0 ^ (-k) ≤ r z ^ (-k) * 0 ^ (-k)

Tactic:
· rw [h, Real.rpow_zero, Real.rpow_zero, one_mul]

Goal state after:
case neg
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
h : ¬-k = 0
⊢ 0 ^ (-k) ≤ r z ^ (-k) * 0 ^ (-k)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

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

Tactic:
by
  constructor
  · intro hx
    obtain ⟨k, hk₁, hk₂⟩ := (abs_eval_T_real_eq_one_iff hn x).mp
      ((abs_eq_abs.mpr (.inl hx)).trans abs_one)
    use k
    refine ⟨hk₁, ?_, hk₂⟩
    rw [hk₂, eval_T_real_cos_int_mul_pi_div hn, Int.cast_negOnePow_natCast] at hx
    exact (neg_one_pow_eq_one_iff_even (by grind)).mp hx
  · rintro ⟨k, hk₁, hk₂, hx⟩
    rw [hx, eval_T_real_cos_int_mul_pi_div hn, Int.negOnePow_even k ((Int.even_coe_nat k).mpr hk₂)]
    norm_cast

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

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

Tactic:
fun_prop

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

Goal state before:
pp: L : PeriodPair
⊢ Meromorphic fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃

Tactic:
fun_prop

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 : (fun k ↦ (↑k + 1) * π / (↑n + 1)) x = (fun k ↦ (↑k + 1) * π / (↑n + 1)) y
⊢ x = y

Tactic:
field_simp at hxy

Goal state after:
case hf
n x : ℕ
hx : x ∈ ↑(Finset.range n)
y : ℕ
hy : y ∈ ↑(Finset.range n)
hxy : ↑x + 1 = ↑y + 1
⊢ x = y
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ AnalyticAt ℂ
    (fun z ↦
      (℘'[L - 0] z * z ^ 3 - 2) ^ 2 - 4 * (℘[L - 0] z * z ^ 2 + 1) ^ 3 + L.g₂ * (℘[L - 0] z * z ^ 6 + z ^ 4) +
        L.g₃ * z ^ 6)
    0

Tactic:
fun_prop

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

Goal state before:
pp: L : PeriodPair
this : 7 ≤ meromorphicOrderAt (L.relation * id ^ 6) 0
⊢ MeromorphicAt L.relation 0

Tactic:
fun_prop

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

Goal state before:
pp: L : PeriodPair
this : 7 ≤ meromorphicOrderAt (L.relation * id ^ 6) 0
⊢ MeromorphicAt (id ^ 6) 0

Tactic:
fun_prop

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

Goal state before:
pp: L : PeriodPair
this : 7 ≤ meromorphicOrderAt L.relation 0 + meromorphicOrderAt (id ^ 6) 0
⊢ MeromorphicAt id 0

Tactic:
fun_prop

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

Goal state before:
pp: L : PeriodPair
⊢ AnalyticAt ℂ (L.relation * id ^ 6) 0

Tactic:
fun_prop

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

Goal state before:
pp: L : PeriodPair
x : ↥L.lattice
this : AnalyticAt ℂ L.relation (↑x - ↑x)
⊢ AnalyticAt ℂ (fun x_1 ↦ x_1 - ↑x) ↑x

Tactic:
fun_prop

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

Goal state before:
pp: L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
this✝ : AnalyticAt ℂ ℘'[L] x
this : AnalyticAt ℂ ℘[L] x
⊢ AnalyticAt ℂ (fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃) x

Tactic:
fun_prop

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

Goal state before:
pp: L : PeriodPair
x : ℂ
⊢ L.relation x = 0 x

Tactic:
have : Differentiable ℂ L.relation := fun x ↦ (L.analyticAt_relation x).differentiableAt

Goal state after:
L : PeriodPair
x : ℂ
this : Differentiable ℂ L.relation
⊢ L.relation x = 0 x
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b u₀ : R
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
ha : 1 < a
h0 : b / (1 - a) < u₀
⊢ Tendsto (fun n ↦ a ^ n * (u₀ - b / (1 - a))) atTop atTop

Tactic:
refine Tendsto.atTop_mul_const (sub_pos.mpr h0) ?_

Goal state after:
R : Type u_1
a b u₀ : R
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
ha : 1 < a
h0 : b / (1 - a) < u₀
⊢ Tendsto (HPow.hPow a) atTop atTop
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
h0 : x ≠ 0
⊢ ∀ (x_1 : ℕ),
    (↑π * x * ∏ j ∈ Finset.range x_1, (1 - x ^ 2 / (↑j + 1) ^ 2)) * (1 / (↑π * x)) =
      ∏ i ∈ Finset.range x_1, (1 + sineTerm x i)

Tactic:
exact fun n ↦ by field_simp; rfl

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

Goal state before:
pp: Z : Set ℂ
hZ : IsCompact Z
⊢ ContinuousOn (fun x ↦ ‖-x ^ 2‖) Z

Tactic:
fun_prop

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

Goal state before:
pp: case refine_2
Z : Set ℂ
hZC : IsCompact Z
u : ℕ → ℝ
hu : Summable u
hu2 : ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j
⊢ ∀ (n : ℕ), ContinuousOn (fun z ↦ sineTerm z n) Z

Tactic:
fun_prop

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

Goal state before:
pp: x : ℂ
k : ℕ∞
hx : x ∈ ℂ_ℤ
⊢ ContDiffWithinAt ℂ (↑k) (fun x ↦ (cexp (↑π * x * I) + cexp (-(↑π * x) * I)) / 2) ℍₒ x

Tactic:
fun_prop

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

Goal state before:
pp: x : ℂ
k : ℕ∞
hx : x ∈ ℂ_ℤ
⊢ ContDiffWithinAt ℂ (↑k) (fun x ↦ (cexp (-(↑π * x) * I) - cexp (↑π * x * I)) * I / 2) ℍₒ x

Tactic:
fun_prop

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

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ DifferentiableOn ℂ (fun z ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) (Set.range Int.cast)ᶜ

Tactic:
fun_prop

Goal state after: