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

Goal state before:
pp: case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → x ∈ closedBall x₀ ↑r → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : E → ℝ → E := fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
hα' : α' = fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
x : E
hx : x ∈ closedBall x₀ ↑r
⊢ α' x ↑t₀ = x

Tactic:
rw [hα']

Goal state after:
case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → x ∈ closedBall x₀ ↑r → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : E → ℝ → E := fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
hα' : α' = fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
x : E
hx : x ∈ closedBall x₀ ↑r
⊢ (fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0) x ↑t₀ = x
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → x ∈ closedBall x₀ ↑r → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : E → ℝ → E := fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
hα' : α' = fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
x : E
hx : x ∈ closedBall x₀ ↑r
t : ℝ
ht : t ∈ Icc tmin tmax
⊢ HasDerivWithinAt (α' x) (f t (α' x t)) (Icc tmin tmax) t

Tactic:
rw [hα']

Goal state after:
case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → x ∈ closedBall x₀ ↑r → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : E → ℝ → E := fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
hα' : α' = fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
x : E
hx : x ∈ closedBall x₀ ↑r
t : ℝ
ht : t ∈ Icc tmin tmax
⊢ HasDerivWithinAt ((fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0) x)
    (f t ((fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0) x t)) (Icc tmin tmax) t
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
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
hv' : ∀ t ∈ Ico (-b) (-a), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))
hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)
hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)
⊢ EqOn f g (Icc a b)

Tactic:
have hmt3 (t : ℝ) : MapsTo Neg.neg (Ici t) (Iic (-t)) :=
    fun _ ht' ↦ mem_Iic.mpr <| neg_le_neg ht'

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
hv' : ∀ t ∈ Ico (-b) (-a), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))
hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)
hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)
hmt3 : ∀ (t : ℝ), MapsTo Neg.neg (Ici t) (Iic (-t))
⊢ EqOn f g (Icc a b)
Module: Mathlib.Analysis.Polynomial.Basic

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

Tactic:
tendsto_const_mul_pow_atTop_iff,

Goal state after:
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x ↦ eval x P) atTop atTop
this : P.natDegree ≠ 0 ∧ 0 < P.leadingCoeff
⊢ 0 < P.degree ∧ 0 ≤ P.leadingCoeff
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case inr.inr.inr
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
⊢ ∀ b ∈ (p + q).support,
    v ((p + q).coeff b) * c ^ b ≤
      max (if h : p.support.Nonempty then p.support.sup' h fun i ↦ v (p.coeff i) * c ^ i else 0)
        (if h : q.support.Nonempty then q.support.sup' h fun i ↦ v (q.coeff i) * c ^ i else 0)

Tactic:
intro i _

Goal state after:
case inr.inr.inr
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 + q).coeff i) * c ^ i ≤
    max (if h : p.support.Nonempty then p.support.sup' h fun i ↦ v (p.coeff i) * c ^ i else 0)
      (if h : q.support.Nonempty then q.support.sup' h fun i ↦ v (q.coeff i) * c ^ i else 0)
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case inr
R : Type u_1
F : Type u_2
inst✝⁴ : Semiring R
inst✝³ : FunLike F R ℝ
v : F
c : ℝ
inst✝² : ZeroHomClass F R ℝ
inst✝¹ : NonnegHomClass F R ℝ
inst✝ : MulHomClass F R ℝ
hna : IsNonarchimedean ⇑v
p q : R[X]
hc : 0 ≤ c
hpq : p * q ≠ 0
h_supp_p : p.support.Nonempty
h_supp_q : q.support.Nonempty
⊢ ∀ b ∈ (p * q).support,
    v (∑ x ∈ range b.succ, p.coeff x * q.coeff (b - x)) * c ^ b ≤
      (p.support.sup' ⋯ fun i ↦ v (p.coeff i) * c ^ i) * q.support.sup' ⋯ fun i ↦ v (q.coeff i) * c ^ i

Tactic:
intro i _

Goal state after:
case inr
R : Type u_1
F : Type u_2
inst✝⁴ : Semiring R
inst✝³ : FunLike F R ℝ
v : F
c : ℝ
inst✝² : ZeroHomClass F R ℝ
inst✝¹ : NonnegHomClass F R ℝ
inst✝ : MulHomClass F R ℝ
hna : IsNonarchimedean ⇑v
p q : R[X]
hc : 0 ≤ c
hpq : p * q ≠ 0
h_supp_p : p.support.Nonempty
h_supp_q : q.support.Nonempty
i : ℕ
a✝ : i ∈ (p * q).support
⊢ v (∑ x ∈ range i.succ, p.coeff x * q.coeff (i - x)) * c ^ i ≤
    (p.support.sup' ⋯ fun i ↦ v (p.coeff i) * c ^ i) * q.support.sup' ⋯ fun i ↦ v (q.coeff i) * c ^ i
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
h : p.degree = 1
⊢ p.logMahlerMeasure = log ‖p.coeff 1‖ + log⁺ ‖(p.coeff 1)⁻¹ * p.coeff 0‖

Tactic:
rw [eq_X_add_C_of_degree_le_one (le_of_eq h)]
  simp [logMahlerMeasure_C_mul_X_add_C (show p.coeff 1 ≠ 0 by exact coeff_ne_zero_of_eq_degree h)]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

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

Tactic:
convert gaussNorm_eq_zero_iff v c f vZero vNonneg h_eq_zero hc hf

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

Goal state before:
pp: ⊢ π < 3.141593

Tactic:
pi_upper_bound [
    35839/25342, 49143/26596, 145729/74292, 294095/147759, 2-137/56868, 2-471/781921, 2-153/1015961,
    2-157/4170049, 2-28/2974805, 2-9/3824747, 2-7/11899211]

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

Goal state before:
pp: f : ℕ → ℝ
h : ofSeq f < 0 ∧ ArchimedeanClass.mk (ofSeq f) < 0
⊢ ∀ (b : ℝ), ∀ᶠ (a : ℕ) in ↑(hyperfilter ℕ), f a ≤ b

Tactic:
exact fun r ↦ ofSeq_le_ofSeq.1 <|
      (lt_of_mk_lt_mk_of_nonpos (h.2.trans_le <| archimedeanClassMk_coe_nonneg r) h.1.le).le

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

Goal state before:
pp: r s : ℝ
hrs : r < s
f : ℕ → ℝ
hxr : (ofSeq f).IsSt r
g : ℕ → ℝ
hys : (ofSeq g).IsSt s
⊢ ofSeq f < ofSeq g

Tactic:
rw [isSt_ofSeq_iff_tendsto] at hxr hys

Goal state after:
r s : ℝ
hrs : r < s
f : ℕ → ℝ
hxr : Tendsto f (↑(hyperfilter ℕ)) (𝓝 r)
g : ℕ → ℝ
hys : Tendsto g (↑(hyperfilter ℕ)) (𝓝 s)
⊢ ofSeq f < ofSeq g
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: r s : ℝ
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : (ofSeq x).IsSt r
y : ℕ → ℝ
hys : (ofSeq y).IsSt s
⊢ IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)

Tactic:
rw [isSt_ofSeq_iff_tendsto] at hxr hys

Goal state after:
r s : ℝ
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : Tendsto x (↑(hyperfilter ℕ)) (𝓝 r)
y : ℕ → ℝ
hys : Tendsto y (↑(hyperfilter ℕ)) (𝓝 s)
⊢ IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
h : ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)
⊢ Tendsto (fun i ↦ (2 * ↑i + 1) / (2 * ↑i + 2)) atTop (𝓝 (1 - 0))

Tactic:
simp_rw [h]

Goal state after:
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
h : ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)
⊢ Tendsto (fun i ↦ 1 - 1 / (2 * ↑i + 2)) atTop (𝓝 (1 - 0))
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

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

Tactic:
calc
    1 < x + 0 := by simpa
    _ ≤ x + √(x ^ 2 - 1) := by gcongr; positivity

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

Goal state before:
pp: x y : ℝ≥0
n : ℕ
⊢ x.agmSequences y (n + 1) =
    (sqrt ((x.agmSequences y n).1 * (x.agmSequences y n).2), ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2)

Tactic:
rw [agmSequences, agmSequences, iterate_succ', comp_apply]

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

Goal state before:
pp: case left
x y : ℝ≥0
h : x ≤ y
⊢ x ≤ sqrt (x * y)

Tactic:
rw [le_sqrt_iff_sq_le, sq]

Goal state after:
case left
x y : ℝ≥0
h : x ≤ y
⊢ x * x ≤ x * y
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case hcd
x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ x ≤ sqrt (x * y)

Tactic:
rw [le_sqrt_iff_sq_le, sq]

Goal state after:
case hcd
x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ x * x ≤ x * y
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
  · simpa [add_comm, mul_comm, dist_comm] using this (not_le.mp h).le
  rw [dist_comm, dist_eq, ← NNReal.coe_sub (sqrt_mul_le_half_add ..), abs_eq]
  calc
    _ ≤ ((x + y) / 2 - x).toReal := by
      gcongr
      rw [le_sqrt_iff_sq_le, sq]
      gcongr
    _ = _ := by
      nth_rw 2 [← add_halves x]
      rw [add_div, add_tsub_add_eq_tsub_left, ← tsub_div, NNReal.coe_div, NNReal.coe_two, dist_comm,
        dist_eq, ← NNReal.coe_sub h, abs_eq]

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

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x ↦ -I / 2 * (((-1) ^ (x.1 * 2 + ↑x.2 + 1) + 1) * (z * I) ^ (x.1 * 2 + ↑x.2) / ↑(x.1 * 2 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
⊢ HasSum (fun n ↦ (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) z.arctan

Tactic:
← mul_comm 2 _

Goal state after:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x ↦ -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
⊢ HasSum (fun n ↦ (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) z.arctan
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt

Goal state before:
pp: case neg
A : Type u_1
inst✝⁸ : PartialOrder A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : SeparatelyContinuousMul A
c a b : A
hab : a ≤ b
hc : ¬0 ≤ c
⊢ (conjSqrt c) a ≤ (conjSqrt c) b

Tactic:
· simp [conjSqrt_of_not_nonneg hc]

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

Goal state before:
pp: n : ℕ
⊢ 0 < I n (π / 2)

Tactic:
refine integral_pos (by simp) (by fun_prop) ?_ ⟨0, by simp⟩

Goal state after:
n : ℕ
⊢ ∀ x ∈ Ioc (-1) 1, 0 ≤ (1 - x ^ 2) ^ n * cos (x * (π / 2))
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b c : ℝ
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hc : 0 < c
hsub : uIcc a b ⊆ Ioi 0
hf_cint : IntervalIntegrable f volume (c * a) (c * b)
h : IntervalIntegrable (fun x ↦ f (c * x)) volume (c * a / c) (c * b / c)
⊢ IntervalIntegrable (fun x ↦ f (c * x)) volume a b

Tactic:
mul_div_cancel_left₀ a hc.ne',

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b c : ℝ
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hc : 0 < c
hsub : uIcc a b ⊆ Ioi 0
hf_cint : IntervalIntegrable f volume (c * a) (c * b)
h : IntervalIntegrable (fun x ↦ f (c * x)) volume a (c * b / c)
⊢ IntervalIntegrable (fun x ↦ f (c * x)) volume a b
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: case h.refine_1
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
r : ℝ
hr : r ∈ spectrum ℝ z
this✝ : 0 < r
this : 0 ≤ b * r
⊢ a + b * r ≠ 0 ∨ 0 ≤ -1

Tactic:
cases lt_or_eq_of_le ha <;> grind

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

Goal state before:
pp: n : ℕ
⊢ log (1 + (↑n + 1)⁻¹) < (↑↑n + ↑1)⁻¹

Tactic:
Rat.cast_one,

Goal state after:
n : ℕ
⊢ log (1 + (↑n + 1)⁻¹) < (↑↑n + 1)⁻¹
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ deriv (fun s ↦ Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π) (1 / 2) + γ * √π =
    (deriv (fun s ↦ Gamma (2 * s) * 2 ^ (1 - 2 * s)) (1 / 2) + γ) * √π

Tactic:
deriv_mul_const,

Goal state after:
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ deriv (fun s ↦ Gamma (2 * s) * 2 ^ (1 - 2 * s)) (1 / 2) * √π + γ * √π =
    (deriv (fun s ↦ Gamma (2 * s) * 2 ^ (1 - 2 * s)) (1 / 2) + γ) * √π

case hc
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ (fun s ↦ Gamma (2 * s) * 2 ^ (1 - 2 * s)) (1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ log (b ^ logb b x) = log |x|

Tactic:
log_rpow b_pos,

Goal state after:
case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ logb b x * log b = log |x|
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
⊢ μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed ↔ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed

Tactic:
by
  constructor <;> intro h A hA r hr
  · obtain ⟨K, hK1, ⟨hK2, _⟩, hK4⟩ := h hA r hr
    refine ⟨K, hK1, ?_, hK4⟩
    simp only [Function.comp_apply]
    exact hK2.closure
  · obtain ⟨K, hK1, hK2, hK3⟩ := h hA r hr
    refine ⟨closure K, closure_minimal hK1 hA, ?_, ?_⟩
    · simpa only [isClosed_closure, and_true]
    · exact hK3.trans_le (measure_mono subset_closure)

Goal state after:
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]

Goal state after:
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ P.InnerRegularWRT (IsCompact ∘ closure) IsClosed
Module: Mathlib.Analysis.SpecialFunctions.Pochhammer

Goal state before:
pp: k n : ℕ
⊢ ↑k ∉ Set.Ici (↑n - 1) → 0 ↑k = ↑(k.descFactorial n)

Tactic:
Set.mem_Ici,

Goal state after:
k n : ℕ
⊢ ¬↑n - 1 ≤ ↑k → 0 ↑k = ↑(k.descFactorial n)
Module: Mathlib.Analysis.SpecialFunctions.Pochhammer

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ ConvexOn ℝ Set.univ ((Set.Ici (↑n - 1)).piecewise (fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) 0)

Tactic:
by
  rw [← Nat.pos_iff_ne_zero] at hn
  apply convexOn_univ_piecewise_Ici_of_monotoneOn_Ici_antitoneOn_Iic
    (convexOn_descPochhammer_eval n) (convexOn_const 0 (convex_Iic (n - 1 : ℝ)))
    (monotoneOn_descPochhammer_eval n) antitoneOn_const
  simpa [← Nat.cast_pred hn] using descPochhammer_eval_coe_nat_of_lt (Nat.sub_one_lt_of_lt hn)

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
a : ℕ
⊢ n.nthRoot (a ^ n) = a

Tactic:
refine eq_of_forall_le_iff fun b ↦ ?_

Goal state after:
n : ℕ
hn : n ≠ 0
a b : ℕ
⊢ b ≤ n.nthRoot (a ^ n) ↔ b ≤ a
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n a b : ℕ
h₁ : a ^ n ≤ b
h₂ : b < (a + 1) ^ n
⊢ n.nthRoot b = a

Tactic:
by
  rcases eq_or_ne n 0 with rfl | hn
  · grind
  simp only [← le_nthRoot_iff hn, ← nthRoot_lt_iff hn] at h₁ h₂
  grind

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

Goal state before:
pp: a b : Multiset ℂ
⊢ (regularizedHGFunSeries a b).coeff = regularizedHGFunCoeff a b

Tactic:
by
  unfold regularizedHGFunSeries
  ext; simp

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : ¬Countable α
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)

Tactic:
· refine
      ⟨univ, MeasurableSet.univ,
        ⟨(PolishSpace.measurableEquivOfNotCountable hα ?_ : α ≃ᵐ (univ : Set ℝ))⟩⟩
    rw [countable_coe_iff]
    exact Cardinal.not_countable_real

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

Goal state before:
pp: x : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
x✝ : ℝ
⊢ 0 ≤ x✝.sigmoid

Tactic:
by bound

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

Goal state before:
pp: x : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
x✝ : ℝ
⊢ x✝.sigmoid ≤ 1

Tactic:
by bound

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

Goal state before:
pp: ⊢ Subtype.val ⁻¹' range Real.sigmoid = Ioo 0 1

Tactic:
Real.range_sigmoid

Goal state after:
⊢ Subtype.val ⁻¹' Ioo 0 1 = Ioo 0 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: θ : ℂ
n : ℤ
⊢ eval (2 * cos θ) (C ℂ n) = 2 * cos (↑n * θ)

Tactic:
simp [C_eq_two_mul_T_comp_half_mul_X]

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

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

Tactic:
L.weierstrassP_add_coe,

Goal state after:
L : PeriodPair
l : ↥L.lattice
⊢ ℘[L] 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: θ : ℂ
n : ℤ
⊢ eval (2 * cosh θ) (C ℂ n) = 2 * cosh (↑n * θ)

Tactic:
simp [C_eq_two_mul_T_comp_half_mul_X]

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

Goal state before:
pp: case e'_5
L : PeriodPair
l : ↥L.lattice
z : ℂ
⊢ -2 / (z - ↑l) ^ 3 = if ↑l = L.ω₁ / 2 then 0 else -2 / (z - ↑l) ^ 3

pp: case e'_6
L : PeriodPair
⊢ ℘'[L] = ℘'[L - L.ω₁ / 2]

Tactic:
· rw [if_neg, neg_div]; exact fun e ↦ L.ω₁_div_two_notMem_lattice (e ▸ l.2)

Goal state after:
case e'_6
L : PeriodPair
⊢ ℘'[L] = ℘'[L - L.ω₁ / 2]
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ IsIntegral ℤ (cexp (-(↑q * ↑π) * I))

Tactic:
simpa using isIntegral_exp_rat_mul_pi_mul_I (-q)

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hr : 0 ≤ r
hr' : r ≤ 1
⊢ ↑r * π ∈ Set.Icc (0 * π) (1 * π)

Tactic:
constructor <;> gcongr

Goal state after:
case hbc
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hr : 0 ≤ r
hr' : r ≤ 1
⊢ 0 ≤ ↑r

case hbc
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hr : 0 ≤ r
hr' : r ≤ 1
⊢ ↑r ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n k : ℕ
hk : k < n
⊢ Multiset.count (cos ((2 * ↑k + 1) * π / (2 * ↑n))) (T ℝ ↑n).roots = 1

Tactic:
roots_T_real,

Goal state after:
n k : ℕ
hk : k < n
⊢ Multiset.count (cos ((2 * ↑k + 1) * π / (2 * ↑n)))
      (Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)).val =
    1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
x : ℝ
hroot : x ∈ (T ℝ ↑n).roots
hnz : x ≠ 0
⊢ Irrational x

Tactic:
roots_T_real,

Goal state after:
n : ℕ
x : ℝ
hroot : x ∈ (Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)).val
hnz : x ≠ 0
⊢ Irrational x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
h0 : x ≠ 0
⊢ Tendsto (fun n ↦ ∏ i ∈ Finset.range n, (1 + sineTerm x i)) atTop (𝓝 (Complex.sin (↑π * x) / (↑π * x)))

Tactic:
by
  rw [show (sin (π * x) / (π * x)) = sin (π * x) * (1 / (π * x)) by ring]
  apply (Filter.Tendsto.mul_const (b := 1 / (π * x)) (tendsto_euler_sin_prod x)).congr
  exact fun n ↦ by field_simp; rfl

Goal state after: