mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case pos.succ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
heqon : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ x₀ α t
hlt : tmin < tmax
this : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (picard f t₀ x₀ α) (f t (α t)) (Icc tmin tmax) t
n : ℕ
hn : ContDiffOn ℝ (↑n) (uncurry f) (Icc tmin tmax ×ˢ u) → ContDiffOn ℝ (↑n) (picard f t₀ x₀ α) (Icc tmin tmax)
hf : ContDiffOn ℝ (↑n + 1) (uncurry f) (Icc tmin tmax ×ˢ u)
⊢ ContDiffOn ℝ (↑n) (derivWithin (picard f t₀ x₀ α) (Icc tmin tmax)) (Icc tmin tmax)

Tactic:
apply contDiffOn_comp hf.of_succ (ContDiffOn.congr (hn hf.of_succ) heqon) hmem |>.congr

Goal state after:
case pos.succ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
heqon : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ x₀ α t
hlt : tmin < tmax
this : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (picard f t₀ x₀ α) (f t (α t)) (Icc tmin tmax) t
n : ℕ
hn : ContDiffOn ℝ (↑n) (uncurry f) (Icc tmin tmax ×ˢ u) → ContDiffOn ℝ (↑n) (picard f t₀ x₀ α) (Icc tmin tmax)
hf : ContDiffOn ℝ (↑n + 1) (uncurry f) (Icc tmin tmax ×ˢ u)
⊢ ∀ x ∈ Icc tmin tmax, derivWithin (picard f t₀ x₀ α) (Icc tmin tmax) x = f x (α x)
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
p : R[X]
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
⊢ gaussNorm v 0 p = v (p.coeff 0)

Tactic:
have : (fun i ↦ v (p.coeff i) * 0 ^ i) = fun i ↦ if i = 0 then v (p.coeff 0) else 0 := by
    aesop

Goal state after:
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
p : R[X]
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
this : (fun i ↦ v (p.coeff i) * 0 ^ i) = fun i ↦ if i = 0 then v (p.coeff 0) else 0
⊢ gaussNorm v 0 p = v (p.coeff 0)
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
hna : IsNonarchimedean ⇑v
c : ℝ
hc : 0 ≤ c
p q : R[X]
h✝¹ : p ≠ 0
h✝ : q ≠ 0
hpq : p + q ≠ 0
i : ℕ
a✝ : i ∈ (p + q).support
⊢ max (v (p.coeff i)) (v (q.coeff i)) * c ^ i = max (v (p.coeff i) * c ^ i) (v (q.coeff i) * c ^ i)

Tactic:
max_mul_of_nonneg _ _ (pow_nonneg hc _)

Goal state after:
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
hna : IsNonarchimedean ⇑v
c : ℝ
hc : 0 ≤ c
p q : R[X]
h✝¹ : p ≠ 0
h✝ : q ≠ 0
hpq : p + q ≠ 0
i : ℕ
a✝ : i ∈ (p + q).support
⊢ max (v (p.coeff i) * c ^ i) (v (q.coeff i) * c ^ i) = max (v (p.coeff i) * c ^ i) (v (q.coeff i) * c ^ i)
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:

Tactic:
v ((p + q).coeff i) * c ^ i
    ≤ max (v (p.coeff i)) (v (q.coeff i)) * c ^ i := by
    rw [coeff_add]
    gcongr
    exact hna (p.coeff i) (q.coeff i)
  _ = max (v (p.coeff i) * c ^ i) (v (q.coeff i) * c ^ i) := by
    rw [max_mul_of_nonneg _ _ (pow_nonneg hc _)]
  _ ≤ max (gaussNorm v c p) (gaussNorm v c q) := by
    apply max_le_max <;>
    exact le_gaussNorm v _ hc i

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: ⊢ logMahlerMeasure 0 = 0

Tactic:
by
  simp [logMahlerMeasure_def, circleAverage_def]

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: ⊢ logMahlerMeasure 1 = 0

Tactic:
by
  simp [logMahlerMeasure_def, circleAverage_def]

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: ⊢ X.logMahlerMeasure = 0

Tactic:
by
  simp [logMahlerMeasure_def, circleAverage_def]

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg.e_a
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
⊢ MeasureTheory.volume
      {a |
        ¬(a ∈ Set.uIoc 0 (2 * π) →
            log (‖eval (circleMap 0 1 a) p‖ * ‖eval (circleMap 0 1 a) q‖) =
              log ‖eval (circleMap 0 1 a) p‖ + log ‖eval (circleMap 0 1 a) q‖)} =
    0

Tactic:
apply Set.Finite.measure_zero _ MeasureTheory.volume

Goal state after:
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
⊢ {a |
      ¬(a ∈ Set.uIoc 0 (2 * π) →
          log (‖eval (circleMap 0 1 a) p‖ * ‖eval (circleMap 0 1 a) q‖) =
            log ‖eval (circleMap 0 1 a) p‖ + log ‖eval (circleMap 0 1 a) q‖)}.Finite
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
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
hf1 : gaussNorm v c f ≠ 0
⊢ gaussNorm v c (f * g) = gaussNorm v c f * gaussNorm v c g

Tactic:
have hg1 : gaussNorm v c g ≠ 0 := by
    convert gaussNorm_eq_zero_iff v c g vZero vNonneg h_eq_zero hc hg
    grind

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
hf1 : gaussNorm v c f ≠ 0
hg1 : gaussNorm v c g ≠ 0
⊢ gaussNorm v c (f * g) = gaussNorm v c f * gaussNorm v c g
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case e'_4
b : ℕ
digits : ℕ → Fin b
hb : 1 < ↑b
⊢ 1 = ∑' (n : ℕ), (↑b - 1) * (↑b ^ (n + 1))⁻¹

pp: case inr.convert_1
b : ℕ
digits : ℕ → Fin b
hb : 1 < ↑b
⊢ Summable fun x ↦ (↑b - 1) * (↑b ^ (x + 1))⁻¹

Tactic:
· simp_rw [pow_succ', mul_inv, ← inv_pow, ← mul_assoc]
    rw [tsum_mul_left, tsum_geometric_of_lt_one (by positivity) (by simp [inv_lt_one_iff₀, hb])]
    have := sub_pos.mpr hb
    field

Goal state after:
case inr.convert_1
b : ℕ
digits : ℕ → Fin b
hb : 1 < ↑b
⊢ Summable fun x ↦ (↑b - 1) * (↑b ^ (x + 1))⁻¹
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: ⊢ π < ↑3 + 1

Tactic:
exact_mod_cast pi_lt_four

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

Goal state before:
pp: case succ
k : ℕ
hk : 0 < W k
⊢ 0 < W (k + 1)

Tactic:
rw [W_succ]
    refine mul_pos hk (mul_pos (div_pos ?_ ?_) (div_pos ?_ ?_)) <;> positivity

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case inl
z : ℂ
k : ℤ
nr : z.re = ↑1 * π / 2
h₂ : 2 * k + 1 ≤ 1
h₁ : -1 < 2 * k + 1
⊢ z.re = π / 2

Tactic:
Int.cast_one,

Goal state after:
case inl
z : ℂ
k : ℤ
nr : z.re = 1 * π / 2
h₂ : 2 * k + 1 ≤ 1
h₁ : -1 < 2 * k + 1
⊢ z.re = π / 2
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo (-1) 1
⊢ sinh (artanh x) = x / √(1 - x ^ 2)

Tactic:
by
  have : 0 < √((1 + x) / (1 - x)) := sqrt_pos_of_pos <| div_pos (by grind) (by grind)
  rw [← one_pow, sq_sub_sq 1 x, sqrt_mul]
    <;> grind [artanh, sinh_eq, exp_neg, exp_log, sqrt_div]

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

Goal state before:
pp: case succ
k : ℝ≥0
n : ℕ
ih : ∀ {x y : ℝ≥0}, ((k * x).agmSequences (k * y) n).2 = k * (x.agmSequences y n).2
x y : ℝ≥0
⊢ ((k * x).agmSequences (k * y) (n + 1)).2 = k * (x.agmSequences y (n + 1)).2

Tactic:
agmSequences_succ,

Goal state after:
case succ
k : ℝ≥0
n : ℕ
ih : ∀ {x y : ℝ≥0}, ((k * x).agmSequences (k * y) n).2 = k * (x.agmSequences y n).2
x y : ℝ≥0
⊢ ((sqrt (k * x * (k * y))).agmSequences ((k * x + k * y) / 2) n).2 = k * (x.agmSequences y (n + 1)).2
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
⊢ Tendsto (fun p ↦ ∫ (x : ℝ) in p.1..p.2, x⁻¹ • (f (a * x) - f (b * x))) (𝓝[>] 0 ×ˢ atTop) (𝓝 (log (b / a) • (L - R)))

Tactic:
by
  let u := fun x ↦ x⁻¹ • f x
  have hint {p q : ℝ} (hp : 0 < p) (hq : 0 < q) : IntervalIntegrable u volume p q :=
    intervalIntegrable_inv_smul hf hp hq
  have hsplit {ε r : ℝ} (hε : 0 < ε) (hr : 0 < r) :
      ∫ x in ε..r, x⁻¹ • (f (a * x) - f (b * x)) =
      (∫ x in (a * ε)..(b * ε), u x) - ∫ x in (a * r)..(b * r), u x := by
    calc ∫ x in ε..r, x⁻¹ • (f (a * x) - f (b * x))
      _ = (∫ x in ε..r, x⁻¹ • f (a * x)) - ∫ x in ε..r, x⁻¹ • f (b * x) := by
        simp_rw [smul_sub]
        exact integral_sub (intervalIntegrable_inv_smul_comp_mul hf hε hr ha)
          (intervalIntegrable_inv_smul_comp_mul hf hε hr hb)
      _ = (∫ y in a * ε..a * r, u y) - ∫ y in b * ε..b * r, u y := by
        rw [integral_comp_mul_inv_smul ha.ne', integral_comp_mul_inv_smul hb.ne']
      _ = _ := integral_interval_sub_interval_comm
                 (hint (mul_pos ha hε) (mul_pos ha hr))
                 (hint (mul_pos hb hε) (mul_pos hb hr))
                 (hint (mul_pos ha hε) (mul_pos hb hε))
  have h_ev : (fun p : ℝ × ℝ ↦ ∫ x in p.1..p.2, x⁻¹ • (f (a * x) - f (b * x))) =ᶠ[(𝓝[>] 0) ×ˢ atTop]
      fun p ↦ (∫ x in (a * p.1)..(b * p.1), u x) - ∫ x in (a * p.2)..(b * p.2), u x := by
    filter_upwards [prod_mem_prod (eventually_nhdsWithin_of_forall fun _ h ↦ h)
      (eventually_atTop.2 ⟨1, fun _ h ↦ lt_of_lt_of_le one_pos h⟩)] with ⟨ε, r⟩ ⟨hε, hr⟩
    exact hsplit hε hr
  rw [tendsto_congr' h_ev, show log (b / a) • (L - R) =
    log (b / a) • L - log (b / a) • R from smul_sub _ _ _]
  exact ((tendsto_integral_inv_smul_nhdsWithin hf ha hb hL).comp tendsto_fst).sub
    ((tendsto_integral_inv_smul_atTop hf ha hb hR).comp tendsto_snd)

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

Goal state before:
pp: s : ℂ
hs : s ≠ 0
⊢ ↑π ^ (-(s + 2) / 2) * Gamma ((s + 2) / 2) = ↑π ^ (-s / 2) * Gamma (s / 2) * s / 2 / ↑π

Tactic:
neg_div,

Goal state after:
s : ℂ
hs : s ≠ 0
⊢ ↑π ^ (-((s + 2) / 2)) * Gamma ((s + 2) / 2) = ↑π ^ (-s / 2) * Gamma (s / 2) * s / 2 / ↑π
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 0 1
s : Set ℝ
hs : s ⊆ Ici 0
⊢ ContinuousOn (Function.uncurry p.rpowIntegrand₀₁) (Ioi 0 ×ˢ s)

Tactic:
by
  let g : ℝ × ℝ → ℝ := fun q => q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
  refine ContinuousOn.congr (f := g) ?_ fun q => ?_
  · simp only [g]
    refine ContinuousOn.mul ?_ ?_
    · refine ContinuousOn.mul ?_ (by fun_prop)
      exact ContinuousOn.rpow_const (by fun_prop) (by grind)
    · exact ContinuousOn.inv₀ (by fun_prop) (by grind)
  · intro hq
    simp [Function.uncurry, g, rpowIntegrand₀₁_eq_pow_div hp (le_of_lt hq.1) (hs hq.2)]

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

Goal state before:
pp: case pos
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s = 1
⊢ 1⁻¹ = Gammaℂ 1 * sin (↑π * 1 / 2) * (↑π ^ (-(1 + 1) / 2) * Gamma ((1 + 1) / 2))⁻¹

Tactic:
neg_div,

Goal state after:
case pos
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s = 1
⊢ 1⁻¹ = Gammaℂ 1 * sin (↑π * 1 / 2) * (↑π ^ (-((1 + 1) / 2)) * Gamma ((1 + 1) / 2))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 0 1
⊢ 0 < -1 / (2 * (p - 1))

Tactic:
neg_div,

Goal state after:
p : ℝ
hp : p ∈ Ioo 0 1
⊢ 0 < -(1 / (2 * (p - 1)))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 1 2
ht : 0 < t
⊢ MonotoneOn (p.rpowIntegrand₁₂ t) (Ici 0)

Tactic:
by
  refine MonotoneOn.congr ?_ fun x hx ↦ (rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ hx ht).symm
  apply monotoneOn_id.mul <;> grind [rpowIntegrand₀₁_monotoneOn, rpowIntegrand₀₁_nonneg]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
h2 : 0 < (↑π / a).re
f_bd : f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
this : ∀ (x : ℝ), -↑π / a * (↑x + I * b) ^ 2 = -↑π / a * ↑x ^ 2 + -2 * ↑π * I * b / a * ↑x + ↑π * b ^ 2 / a
⊢ (-↑π / a).re < 0

Tactic:
neg_div,

Goal state after:
a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
h2 : 0 < (↑π / a).re
f_bd : f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
this : ∀ (x : ℝ), -↑π / a * (↑x + I * b) ^ 2 = -↑π / a * ↑x ^ 2 + -2 * ↑π * I * b / a * ↑x + ↑π * b ^ 2 / a
⊢ (-(↑π / a)).re < 0
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
this : HasDerivAt (fun x ↦ ↑π ^ (-x / 2)) (↑π ^ (-1 / 2) * log ↑π * (-1 / 2)) 1
⊢ ↑π ^ (-1 / 2) * (-log ↑π / 2) = -log ↑π / 2 / ↑√π

Tactic:
neg_div,

Goal state after:
f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
this : HasDerivAt (fun x ↦ ↑π ^ (-x / 2)) (↑π ^ (-1 / 2) * log ↑π * (-1 / 2)) 1
⊢ ↑π ^ (-(1 / 2)) * (-log ↑π / 2) = -log ↑π / 2 / ↑√π
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: case refine_2
f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
this : HasDerivAt (Gamma ∘ fun s ↦ s / 2) (-↑√π * (↑γ + 2 * log 2) * (1 / 2)) 1
⊢ HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1

Tactic:
rwa [mul_one_div] at this

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
x : A
hx : x ∈ Ici 0
hg : ContinuousOn (fun z ↦ (t + z)⁻¹) (spectrum ℝ x)
hf : ContinuousOn (fun z ↦ 1 + z) (spectrum ℝ x)
hspectrum : ∀ r ∈ spectrum ℝ x, t + r ≠ 0
this : cfc (fun x ↦ t ^ (p - 1) - t ^ p * (t + x)⁻¹) x = cfc (fun x ↦ t ^ (p - 1)) x - cfc (fun z ↦ t ^ p * (t + z)⁻¹) x
⊢ cfc (fun x ↦ t ^ (p - 1)) x - cfc (fun z ↦ t ^ p * (t + z)⁻¹) x =
    (fun x ↦ (algebraMap ℝ A) (t ^ (p - 1)) - t ^ p • Ring.inverse ((algebraMap ℝ A) t + x)) x

Tactic:
cfc_const ..,

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
x : A
hx : x ∈ Ici 0
hg : ContinuousOn (fun z ↦ (t + z)⁻¹) (spectrum ℝ x)
hf : ContinuousOn (fun z ↦ 1 + z) (spectrum ℝ x)
hspectrum : ∀ r ∈ spectrum ℝ x, t + r ≠ 0
this : cfc (fun x ↦ t ^ (p - 1) - t ^ p * (t + x)⁻¹) x = cfc (fun x ↦ t ^ (p - 1)) x - cfc (fun z ↦ t ^ p * (t + z)⁻¹) x
⊢ (algebraMap ℝ A) (t ^ (p - 1)) - cfc (fun z ↦ t ^ p * (t + z)⁻¹) x =
    (fun x ↦ (algebraMap ℝ A) (t ^ (p - 1)) - t ^ p • Ring.inverse ((algebraMap ℝ A) t + x)) x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
hb : 1 < b
hx : 0 < x
⊢ logb b 1 < logb b x ↔ 1 < x

Tactic:
logb_lt_logb_iff hb zero_lt_one hx

Goal state after:
b x : ℝ
hb : 1 < b
hx : 0 < x
⊢ 1 < x ↔ 1 < x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b : ℝ
hb : 1 < b
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ |y| < |x|

Tactic:
abs_of_neg hy,

Goal state after:
b : ℝ
hb : 1 < b
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ -y < |x|
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

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

Tactic:
abs_of_neg hy,

Goal state after:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ -y < |x|
Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone

Goal state before:
pp: a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
x✝ : y ∈ Ici (rexp a⁻¹)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ log (y ^ 1) / y ^ a ≤ log (x ^ 1) / x ^ a

Tactic:
← div_self (ne_of_lt ha).symm,

Goal state after:
a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
x✝ : y ∈ Ici (rexp a⁻¹)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ log (y ^ (a / a)) / y ^ a ≤ log (x ^ (a / a)) / x ^ a
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case pos
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
⊢ ⌈logb (↑b) r⌉ = Int.clog b r

Tactic:
have hb1' : 1 < (b : ℝ) := Nat.one_lt_cast.mpr hb
    apply le_antisymm
    · rw [Int.ceil_le, logb_le_iff_le_rpow hb1' hr, rpow_intCast]
      exact Int.self_le_zpow_clog hb r
    · rw [← Int.le_zpow_iff_clog_le hb hr, ← rpow_intCast b]
      refine (rpow_logb (zero_lt_one.trans hb1') hb1'.ne' hr).symm.trans_le ?_
      exact rpow_le_rpow_of_exponent_le hb1'.le (Int.le_ceil _)

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, p K ∧ μ Kᶜ < ε
⊢ μ.InnerRegularWRT p q

Tactic:
intro A hA r hr

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, p K ∧ μ Kᶜ < ε
A : Set α
hA : q A
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K ⊆ A, p K ∧ r < μ K
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
⊢ P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed

Tactic:
rw [innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure]
  exact innerRegularWRT_isCompact_closure P

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

Goal state before:
pp: n : ℕ
ε : ℝ
⊢ 0 < toSphereBallBound n ε

Tactic:
unfold toSphereBallBound

Goal state after:
n : ℕ
ε : ℝ
⊢ 0 < if n ≠ 0 ∧ 0 < ε then ↑n * (min ε.toNNReal 2 / 4) ^ n else 1
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
⊢ ‖1 / (s - l) ^ 2 - 1 / l ^ 2‖ ≤ 10 * r * ‖l‖ ^ (-3)

Tactic:
by
  have : s ≠ ↑l := by rintro rfl; linarith
  have : 0 < ‖l‖ := by linarith
  calc
    _ = ‖(↑l ^ 2 - (s - ↑l) ^ 2) / ((s - ↑l) ^ 2 * ↑l ^ 2)‖ := by
      rw [div_sub_div, one_mul, mul_one]
      · simpa [sub_eq_zero]
      · simpa
    _ = ‖l ^ 2 - (s - l) ^ 2‖ / (‖s - l‖ ^ 2 * ‖l‖ ^ 2) := by simp
    _ ≤ ‖l ^ 2 - (s - l) ^ 2‖ / ((‖l‖ / 2) ^ 2 * ‖l‖ ^ 2) := by
      gcongr
      rw [norm_sub_rev]
      exact .trans (by linarith) (norm_sub_norm_le l s)
    _ = ‖s * (2 * l - s)‖ / (‖l‖ ^ 4 / 4) := by
      congr 1
      · rw [sq_sub_sq]; simp [← sub_add, two_mul, sub_add_eq_add_sub]
      · ring
    _ = (‖s‖ * ‖2 * l - s‖) / (‖l‖ ^ 4 / 4) := by simp
    _ = (4 * ‖s‖ * ‖2 * l - s‖) / ‖l‖ ^ 4 := by field
    _ ≤ (4 * r * (2.5 * ‖l‖)) / ‖l‖ ^ 4 := by
      gcongr (4 * ?_ * ?_) / ‖l‖ ^ 4
      refine (norm_sub_le _ _).trans ?_
      simp only [Complex.norm_mul, Complex.norm_ofNat]
      linarith
    _ = 10 * r / ‖l‖ ^ 3 := by field
    _ = _ := by norm_cast

Goal state after:
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 1 / (z - ↑b) ^ 2 - 1 / ↑b ^ 2) +
        if ↑b = ↑l₀ then 1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2 else 0) =
    ℘[L] z

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

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

Goal state before:
pp: L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ℘[L - ↑l₀] z = ℘[L] z + (1 / ↑l₀ ^ 2 - 1 / (z - ↑l₀) ^ 2)

Tactic:
rw [← L.weierstrassPExcept_add l₀]

Goal state after:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ℘[L - ↑l₀] z = ℘[L - ↑l₀] z + (1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2) + (1 / ↑l₀ ^ 2 - 1 / (z - ↑l₀) ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

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

Tactic:
simp only [Equiv.neg_apply, NegMemClass.coe_neg, sub_neg_eq_add, neg_add_eq_sub,
    ← div_neg, ← tsum_neg, apply_ite, neg_zero]

Goal state after:
L : PeriodPair
l₀ z : ℂ
⊢ (∑' (c : ↥L.lattice), if -↑c = l₀ then 0 else -2 / (↑c - z) ^ 3) =
    ∑' (b : ↥L.lattice), if ↑b = -l₀ then 0 else -2 / -(z - ↑b) ^ 3
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: case inr
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : (-1) ^ (-k) = (-1) ^ k
⊢ Complex.exp (↑k / (2 * ↑n) * ↑π * I) / (Complex.exp (↑k / ↑n * ↑π * I) - 1) * ((-1) ^ k - 1) +
      Complex.exp (-↑k / (2 * ↑n) * ↑π * I) / (Complex.exp (-↑k / ↑n * ↑π * I) - 1) * ((-1) ^ (-k) - 1) =
    0

Tactic:
neg_div,

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

Goal state before:
pp: case inr
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : (-1) ^ (-k) = (-1) ^ k
⊢ Complex.exp (↑k / (2 * ↑n) * ↑π * I) / (Complex.exp (↑k / ↑n * ↑π * I) - 1) * ((-1) ^ k - 1) +
      (Complex.exp (↑k / (2 * ↑n) * ↑π * I))⁻¹ / (Complex.exp (-↑k / ↑n * ↑π * I) - 1) * ((-1) ^ (-k) - 1) =
    0

Tactic:
neg_div,

Goal state after:
case inr
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : (-1) ^ (-k) = (-1) ^ k
⊢ Complex.exp (↑k / (2 * ↑n) * ↑π * I) / (Complex.exp (↑k / ↑n * ↑π * I) - 1) * ((-1) ^ k - 1) +
      (Complex.exp (↑k / (2 * ↑n) * ↑π * I))⁻¹ / (Complex.exp (-(↑k / ↑n) * ↑π * I) - 1) * ((-1) ^ (-k) - 1) =
    0
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)
⊢ ∫ (x : ℝ), eval x P ∂measureT = sumZeroes n P

Tactic:
← Sequence.span_degreeLT (chebyshevTsequence ℝ) (by simp),

Goal state after:
n : ℕ
P : ℝ[X]
hn : n ≠ 0
hP : P.degree < 2 * ↑n
hmem : P ∈ Submodule.span ℝ (↑(chebyshevTsequence ℝ) '' Set.Iio (2 * n))
⊢ ∫ (x : ℝ), eval x P ∂measureT = sumZeroes n P
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
⊢ P.coeff n ≤ 2 ^ (n - 1)

Tactic:
by
  convert! sumNodes_le_sumNodes_T (fun i hi => le_of_lt <| negOnePow_mul_leadingCoeffC_pos hi) hPbnd
  · rw [sumNodes_eq_coeff hPdeg]
  · rw [sumNodes_T_eq]

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

Goal state before:
pp: x : Fin 2 → ℤ
hx : ↑(x 0).natAbs ≠ 0
H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs
⊢ x 0 ≠ 0

Tactic:
Nat.cast_ne_zero,

Goal state after:
x : Fin 2 → ℤ
hx : (x 0).natAbs ≠ 0
H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs
⊢ x 0 ≠ 0