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

Goal state before:
pp: case mk
E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L : ℝ≥0
β : FunSpace t₀ x₀ r L
toFun✝ : ↑(Icc tmin tmax) → E
lipschitzWith✝ : LipschitzWith L toFun✝
mem_closedBall₀✝ : toFun✝ t₀ ∈ closedBall x₀ ↑r
h :
  (fun α ↦ { toFun := α.toFun, continuous_toFun := ⋯ })
      { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ } =
    (fun α ↦ { toFun := α.toFun, continuous_toFun := ⋯ }) β
⊢ { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ } = β

Tactic:
cases β

Goal state after:
case mk.mk
E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L : ℝ≥0
toFun✝¹ : ↑(Icc tmin tmax) → E
lipschitzWith✝¹ : LipschitzWith L toFun✝¹
mem_closedBall₀✝¹ : toFun✝¹ t₀ ∈ closedBall x₀ ↑r
toFun✝ : ↑(Icc tmin tmax) → E
lipschitzWith✝ : LipschitzWith L toFun✝
mem_closedBall₀✝ : toFun✝ t₀ ∈ closedBall x₀ ↑r
h :
  (fun α ↦ { toFun := α.toFun, continuous_toFun := ⋯ })
      { toFun := toFun✝¹, lipschitzWith := lipschitzWith✝¹, mem_closedBall₀ := mem_closedBall₀✝¹ } =
    (fun α ↦ { toFun := α.toFun, continuous_toFun := ⋯ })
      { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ }
⊢ { toFun := toFun✝¹, lipschitzWith := lipschitzWith✝¹, mem_closedBall₀ := mem_closedBall₀✝¹ } =
    { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ }
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
t₀ : ℝ
hv : ∀ᶠ (t : ℝ) in 𝓝 t₀, LipschitzOnWith K (v t) (s t)
hf : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
ε : ℝ
hε : ε > 0
h :
  ∀ y ∈ ball t₀ ε,
    LipschitzOnWith K (v y) (s y) ∧ (HasDerivAt f (v y (f y)) y ∧ f y ∈ s y) ∧ HasDerivAt g (v y (g y)) y ∧ g y ∈ s y
⊢ EqOn f g (ball t₀ ε)

Tactic:
simp_rw [Real.ball_eq_Ioo] at *

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
t₀ : ℝ
hv : ∀ᶠ (t : ℝ) in 𝓝 t₀, LipschitzOnWith K (v t) (s t)
hf : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
ε : ℝ
hε : ε > 0
h :
  ∀ y ∈ Ioo (t₀ - ε) (t₀ + ε),
    LipschitzOnWith K (v y) (s y) ∧ (HasDerivAt f (v y (f y)) y ∧ f y ∈ s y) ∧ HasDerivAt g (v y (g y)) y ∧ g y ∈ s y
⊢ EqOn f g (Ioo (t₀ - ε) (t₀ + ε))
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x ↦ eval x P) atTop (𝓝 c)
this : Tendsto (fun x ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
hP : P.leadingCoeff = 0
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0

pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x ↦ eval x P) atTop (𝓝 c)
this : Tendsto (fun x ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
hP : ¬P.leadingCoeff = 0
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0

Tactic:
· simp only [hP, zero_mul, tendsto_const_nhds_iff] at this
      exact ⟨_root_.trans hP this, by simp [leadingCoeff_eq_zero.1 hP]⟩

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x ↦ eval x P) atTop (𝓝 c)
this : Tendsto (fun x ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
hP : ¬P.leadingCoeff = 0
⊢ P.leadingCoeff = c ∧ P.degree ≤ 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) * c ^ i) (v (q.coeff i) * c ^ i) ≤ max (gaussNorm v c p) (gaussNorm v c q)

Tactic:
apply max_le_max

Goal state after:
case a
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
⊢ v (p.coeff i) * c ^ i ≤ gaussNorm v c p

case a
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
⊢ v (q.coeff i) * c ^ i ≤ gaussNorm v c q
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
hα : IsFixedPt (FunSpace.next hf hx) α
t : ℝ
ht : t ∈ Icc tmin tmax
⊢ picard f (↑t₀) x α.compProj ↑(projIcc tmin tmax ⋯ t) = picard f (↑t₀) x (FunSpace.next hf hx α).compProj t

Tactic:
hα,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
hα : IsFixedPt (FunSpace.next hf hx) α
t : ℝ
ht : t ∈ Icc tmin tmax
⊢ picard f (↑t₀) x α.compProj ↑(projIcc tmin tmax ⋯ t) = picard f (↑t₀) x α.compProj t
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: case inl
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑a ≤ ↑b
⊢ a =ᶠ[↑φ] fun x ↦ min (a x) (b x)

Tactic:
exact h.mono fun i hi => (min_eq_left hi).symm

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

Goal state before:
pp: p : ℂ[X]
⊢ p.mahlerMeasure ≤ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2)

Tactic:
have : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π))) := by
    rw [uIoc_of_le (by positivity)]; infer_instance
  have : NeZero (volume (uIoc 0 (2 * π))) := ⟨by simp⟩
  by_cases! hp : p = 0
  · simp [hp]
  have : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖p.eval (circleMap 0 1 θ)‖ := by
    rw [ae_restrict_iff' measurableSet_uIoc]
    refine Set.Finite.measure_zero ?_ _
    simp only [norm_pos_iff, ne_eq, compl_ofPred, Classical.not_imp, Decidable.not_not]
    refine Finite.of_finite_image (f := circleMap 0 1) (p.roots.finite_toSet.subset ?_) ?_
    · rintro z ⟨θ, ⟨_, heval⟩, rfl⟩
      exact (mem_roots hp).mpr heval
    · grw [ofPred_and, inter_subset_left]
      exact injOn_circleMap_of_abs_sub_le one_ne_zero (by simp [abs_of_pos pi_pos])
  have hlogAe : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)),
      exp (log ‖p.eval (circleMap 0 1 θ)‖) = ‖p.eval (circleMap 0 1 θ)‖ := by
    filter_upwards [this] with θ hθ
    exact exp_log hθ
  have hcont : Continuous (fun x : ℝ ↦ ‖eval (circleMap 0 1 x) p‖) := by fun_prop
  simp only [mahlerMeasure, logMahlerMeasure, ne_eq, hp, not_false_eq_true, ↓reduceIte]
  rw [circleAverage_eq_intervalAverage]
  calc exp (⨍ (θ : ℝ) in 0..(2 * π), log ‖p.eval (circleMap 0 1 θ)‖)
    ≤ ⨍ (θ : ℝ) in 0..(2 * π), exp (log ‖p.eval (circleMap 0 1 θ)‖) := by
        -- First Jensen's inequality invocation
        refine convexOn_exp.map_average_le continuousOn_exp isClosed_univ (by simp) ?_ ?_
        · rw [Set.uIoc_of_le (by positivity : 0 ≤ 2 * Real.pi)]
          exact ((analyticOnNhd_id.aeval_polynomial p).meromorphicOn.circleIntegrable_log_norm).1
        · exact (integrable_congr hlogAe).mpr hcont.integrableOn_uIoc
    _ = ⨍ (θ : ℝ) in 0..(2 * π), ‖p.eval (circleMap 0 1 θ)‖ := average_congr hlogAe
    _ = √((⨍ (θ : ℝ) in 0..(2 * π), ‖p.eval (circleMap 0 1 θ)‖) ^ 2) := by
        rw [sqrt_sq]; exact integral_nonneg (fun _ ↦ norm_nonneg _)
    _ ≤ √(⨍ (θ : ℝ) in 0..(2 * π), ‖p.eval (circleMap 0 1 θ)‖ ^ 2) := by
        -- Second Jensen's inequality invocation
        gcongr
        refine (convexOn_pow 2).map_average_le (continuousOn_pow 2)
            isClosed_Ici (by filter_upwards; simp) ?_ ?_
        · exact hcont.integrableOn_Icc.mono_set Set.Ioc_subset_Icc_self
        · exact ((continuous_pow 2).comp hcont).integrableOn_Icc.mono_set Set.Ioc_subset_Icc_self
    _ = √(circleAverage (fun θ ↦ ‖p.eval θ‖ ^ 2) 0 1) := by simp [circleAverage_eq_intervalAverage]
    _ = √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2) := by simp [p.sum_sq_norm_coeff_eq_circleAverage]

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

Goal state before:
pp: case succ
x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
this : b ≠ 0
n : ℕ
ih : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊
⊢ ↑b * ↑⌊↑b ^ n * x⌋₊ + ↑b * ↑b ^ n * (↑↑(x.digits b n) * (↑b ^ (n + 1))⁻¹) = ↑⌊↑b * ↑b ^ n * x⌋₊

Tactic:
digits,

Goal state after:
case succ
x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
this : b ≠ 0
n : ℕ
ih : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊
⊢ ↑b * ↑⌊↑b ^ n * x⌋₊ + ↑b * ↑b ^ n * (↑↑(Fin.ofNat b ⌊x * ↑b ^ (n + 1)⌋₊) * (↑b ^ (n + 1))⁻¹) = ↑⌊↑b * ↑b ^ n * x⌋₊
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: b : ℕ
inst✝ : NeZero b
⊢ (ofDigits fun x ↦ Fin.last b) = 1

Tactic:
by
  have : 1 < |(b + 1 : ℝ)| := by
    rw [← Nat.cast_add_one, abs_of_nonneg (Nat.cast_nonneg _)]
    simp [NeZero.pos b]
  simp only [ofDigits, ofDigitsTerm, ← inv_pow]
  rw [Summable.tsum_mul_left]
  · rw [geom_series_succ _ (by simp [inv_lt_one_iff₀, this]),
      tsum_geometric_of_lt_one (by positivity) (by simp [inv_lt_one_iff₀, NeZero.pos b])]
    push_cast
    have : (b : ℝ) ≠ 0 := mod_cast NeZero.ne b
    field [*]
  · rw [summable_nat_add_iff (f := fun n ↦ ((b + 1 : ℕ) : ℝ)⁻¹ ^ n) 1]
    apply summable_geometric_of_lt_one (by positivity) (by simp [inv_lt_one_iff₀, NeZero.pos b])

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

Goal state before:
pp: b : ℕ
hb : 1 < b
this : NeZero b
⊢ Set.SurjOn ofDigits Set.univ (Set.Icc 0 1)

Tactic:
intro y

Goal state after:
b : ℕ
hb : 1 < b
this : NeZero b
y : ℝ
⊢ y ∈ Set.Icc 0 1 → y ∈ ofDigits '' Set.univ
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: case inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : C a * X + C b ≠ 0
x_is_root : (aeval x) (C a * X + C b) = 0
this : -↑b / ↑a = x
ha : ¬a = 0
⊢ False

Tactic:
refine hx ⟨-b / a, ?_⟩
      assumption_mod_cast

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

Goal state before:
pp: case right
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
⊢ ∀ ⦃y : ℝ⦄,
    dist y 1 < 1 →
      y ∈ Set.Iio 1 → ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) y * y = arctan y

Tactic:
intro y

Goal state after:
case right
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
⊢ dist y 1 < 1 →
    y ∈ Set.Iio 1 → ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) y * y = arctan y
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ (x + √(x ^ 2 - 1)) * (x - √(x ^ 2 - 1)) = 1

Tactic:
← pow_two_sub_pow_two,

Goal state after:
x : ℝ
hx : 1 ≤ x
⊢ x ^ 2 - √(x ^ 2 - 1) ^ 2 = 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case inr
z : ℂ
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
ni : ¬z.im = 0
⊢ ¬z.re = ↑(2 * k + 1) * π / 2 ∨ ¬z.im = 0

Tactic:
· exact Or.inr ni

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

Goal state before:
pp: x y : ℝ≥0
⊢ dist (sqrt (x * y)) ((x + y) / 2) ≤ dist x y / 2

Tactic:
wlog h : x ≤ y generalizing x y

Goal state after:
case inr
x y : ℝ≥0
this : ∀ {x y : ℝ≥0}, x ≤ y → dist (sqrt (x * y)) ((x + y) / 2) ≤ dist x y / 2
h : ¬x ≤ y
⊢ dist (sqrt (x * y)) ((x + y) / 2) ≤ dist x y / 2

x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ dist (sqrt (x * y)) ((x + y) / 2) ≤ dist x y / 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: x : ℝ
⊢ ↑(Real.arctan x) = (tan ↑(Real.arctan x)).arctan

Tactic:
arctan_tan

Goal state after:
x : ℝ
⊢ ↑(Real.arctan x) = ↑(Real.arctan x)

case h₀
x : ℝ
⊢ ↑(Real.arctan x) ≠ ↑π / 2

case h₁
x : ℝ
⊢ -(π / 2) < (↑(Real.arctan x)).re

case h₂
x : ℝ
⊢ (↑(Real.arctan x)).re ≤ π / 2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
⊢ x.agm y ≤ max x y

Tactic:
wlog h : x ≤ y generalizing x y

Goal state after:
case inr
x y : ℝ≥0
this : ∀ {x y : ℝ≥0}, x ≤ y → x.agm y ≤ max x y
h : ¬x ≤ y
⊢ x.agm y ≤ max x y

x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ x.agm y ≤ max x y
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
n : ℕ
| dist (x.agmSequences y n).2 (x.agmSequences y n).1

Tactic:
rw [dist_comm]

Goal state after:
x y : ℝ≥0
n : ℕ
| dist (x.agmSequences y n).1 (x.agmSequences y n).2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
⊢ min x y ≤ x.agm y

Tactic:
wlog h : x ≤ y generalizing x y

Goal state after:
case inr
x y : ℝ≥0
this : ∀ {x y : ℝ≥0}, x ≤ y → min x y ≤ x.agm y
h : ¬x ≤ y
⊢ min x y ≤ x.agm y

x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ min x y ≤ x.agm y
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
⊢ Continuous (qaryEntropy q)

Tactic:
unfold qaryEntropy; fun_prop

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

Goal state before:
pp: q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ DifferentiableAt ℝ (qaryEntropy q) p

Tactic:
unfold qaryEntropy; fun_prop

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

Goal state before:
pp: case inl
p : ℤ[X]
a : ℤ
k : ℕ
hp : p.natDegree ≤ k
⊢ ∃ z, eval₂ (Int.castRingHom ℝ) (↑a / ↑0) p * ↑0 ^ k = ↑z

pp: case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
⊢ ∃ z, eval₂ (Int.castRingHom ℝ) (↑a / ↑b) p * ↑b ^ k = ↑z

Tactic:
· rcases k.eq_zero_or_pos with rfl | hk
    · exact ⟨p.coeff 0, by simp⟩
    exact ⟨0, by simp [hk.ne']⟩

Goal state after:
case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
⊢ ∃ z, eval₂ (Int.castRingHom ℝ) (↑a / ↑b) p * ↑b ^ k = ↑z
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
s : Set A := {a | IsStrictlyPositive a}
f : ℝ → A → A := fun p a ↦ if a ∈ s then cfc (fun x ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : A → A := fun a ↦ if a ∈ s then log a else 0
hg : Set.EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, f x ∈ {f | MonotoneOn f {a | IsStrictlyPositive a}}

Tactic:
filter_upwards [h₁] with p ⟨hp, hp'⟩

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
s : Set A := {a | IsStrictlyPositive a}
f : ℝ → A → A := fun p a ↦ if a ∈ s then cfc (fun x ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : A → A := fun a ↦ if a ∈ s then log a else 0
hg : Set.EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
⊢ MonotoneOn (f p) {a | IsStrictlyPositive a}
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
s : Set A := {a | IsStrictlyPositive a}
f : ℝ → A → A := fun p a ↦ if a ∈ s then cfc (fun x ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : A → A := fun a ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, f x ∈ {f | ConcaveOn ℝ s f}

Tactic:
filter_upwards [h₁] with p ⟨hp, hp'⟩

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
s : Set A := {a | IsStrictlyPositive a}
f : ℝ → A → A := fun p a ↦ if a ∈ s then cfc (fun x ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : A → A := fun a ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
⊢ ConcaveOn ℝ s (f p)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 0 1
⊢ ∃ μ,
    ∀ a ∈ Ici 0,
      IntegrableOn (fun t ↦ cfcₙ ((↑p).rpowIntegrand₀₁ t) a) (Ioi 0) μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ ((↑p).rpowIntegrand₀₁ t) a ∂μ

Tactic:
obtain ⟨μ, hμ⟩ := exists_measure_rpow_eq_integral_rpowIntegrand₀₁ hp
  refine ⟨μ, fun a (ha : 0 ≤ a) => ?_⟩
  nontriviality A
  have p_pos : 0 < (p : ℝ) := by exact_mod_cast hp.1
  let f t := rpowIntegrand₀₁ p t
  let maxr := sSup (quasispectrum ℝ a)
  have maxr_nonneg : 0 ≤ maxr :=
    le_csSup_of_le (b := 0) (IsCompact.bddAbove (by grind)) (by simp) (by simp)
  let bound (t : ℝ) := ‖f t maxr‖
  have hf : ContinuousOn (Function.uncurry f) (Ioi (0 : ℝ) ×ˢ quasispectrum ℝ a) := by
    refine continuousOn_rpowIntegrand₀₁_uncurry hp (quasispectrum ℝ a) ?_
    grind
  have hbound : ∀ᵐ t ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t := by
    filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht
    intro z hz
    have hz' : 0 ≤ z := by grind
    unfold bound f
    rw [Real.norm_of_nonneg (rpowIntegrand₀₁_nonneg p_pos (le_of_lt ht) hz'),
        Real.norm_of_nonneg (rpowIntegrand₀₁_nonneg p_pos (le_of_lt ht) maxr_nonneg)]
    refine rpowIntegrand₀₁_monotoneOn hp (le_of_lt ht) hz' maxr_nonneg ?_
    exact le_csSup (IsCompact.bddAbove (quasispectrum.isCompact _)) hz
  have hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0)) := by
    rw [hasFiniteIntegral_norm_iff]
    exact (hμ maxr maxr_nonneg).1.2
  have hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), rpowIntegrand₀₁ p x 0 = 0 := by
    filter_upwards [ae_restrict_mem measurableSet_Ioi]
    simp
  refine ⟨?integrable, ?integral⟩
  case integrable =>
    exact integrableOn_cfcₙ measurableSet_Ioi _ bound a hf hmapzero hbound hbound_finite_integral
  case integral => calc
    a ^ p = cfcₙ (fun r => ∫ t in Ioi 0, rpowIntegrand₀₁ p t r ∂μ) a := by
      rw [nnrpow_eq_cfcₙ_real _ _]
      exact cfcₙ_congr fun r _ ↦ (hμ r (by grind)).2
    _ = _ := cfcₙ_setIntegral measurableSet_Ioi _ bound a hf hmapzero hbound
                hbound_finite_integral ha.isSelfAdjoint

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ 0 < ↑b

Tactic:
exact Nat.cast_pos.mpr (zero_le_one.trans_lt hb)

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
h : 0 < x
h₁ : 0 < y
⊢ logb b x ≤ logb b y ↔ y ≤ x

Tactic:
by
  rw [logb, logb, div_le_div_right_of_neg (log_neg b_pos b_lt_one), log_le_log_iff h₁ h]

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
hy : 0 < y
⊢ logb b x < logb b y ↔ y < x

Tactic:
by
  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.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
h_rpow : IntegrableOn (fun y ↦ y ^ (↑(Module.finrank ℝ E) - 1 - α)) (Ioo 0 r) volume
⊢ EqOn (fun x ↦ C * x ^ (↑(Module.finrank ℝ E) - 1 - α)) (fun y ↦ y ^ (Module.finrank ℝ E - 1) * (C * y ^ (-α)))
    (Ioo 0 r)

Tactic:
intro y

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
h_rpow : IntegrableOn (fun y ↦ y ^ (↑(Module.finrank ℝ E) - 1 - α)) (Ioo 0 r) volume
y : ℝ
⊢ y ∈ Ioo 0 r →
    (fun x ↦ C * x ^ (↑(Module.finrank ℝ E) - 1 - α)) y = (fun y ↦ y ^ (Module.finrank ℝ E - 1) * (C * y ^ (-α))) y
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
⊢ ball ((1 - ε / 4) • x) (ε / 4) ⊆ Ioo 0 1 • (ball x ε ∩ sphere 0 1)

Tactic:
intro y

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
⊢ y ∈ ball ((1 - ε / 4) • x) (ε / 4) → y ∈ Ioo 0 1 • (ball x ε ∩ sphere 0 1)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z : ℂ
⊢ ℘[L] (-z) = ℘[L] z

Tactic:
simp only [weierstrassP]

Goal state after:
L : PeriodPair
z : ℂ
⊢ ∑' (l : ↥L.lattice), (1 / (-z - ↑l) ^ 2 - 1 / ↑l ^ 2) = ∑' (l : ↥L.lattice), (1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: case neg.hc'
a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
⊢ Tendsto (fun n ↦ ‖regularizedHGFunCoeff a b n.succ‖ / ‖regularizedHGFunCoeff a b n‖) atTop (𝓝 0)

Tactic:
simp only [Nat.succ_eq_add_one]

Goal state after:
case neg.hc'
a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
⊢ Tendsto (fun n ↦ ‖regularizedHGFunCoeff a b (n + 1)‖ / ‖regularizedHGFunCoeff a b n‖) atTop (𝓝 0)
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
r : ℝ
⊢ Integrable (fun x ↦ (Iio r).indicator f ‖x‖) μ ↔
    IntegrableOn ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) (Ioi 0) volume

Tactic:
by
      rw [integrable_fun_norm_addHaar μ (f := indicator (Iio r) f),
        integrableOn_congr_fun _ measurableSet_Ioi]
      intro x (hx : 0 < x)
      by_cases hxr : x < r <;> simp [hxr, hx]

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
⊢ ℘[L] (z + ↑l) = ℘[L] z

Tactic:
have := L.weierstrassPExcept_add_coe_aux (z + l) (add_mem hz l.2) l hl (x := z) (by simp)
    dsimp at this
    rw [← L.weierstrassPExcept_add ⟨z + l, add_mem hz l.2⟩, this,
      ← L.weierstrassPExcept_add ⟨z, hz⟩]
    simp
    ring

Goal state after: