mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
n : ℕ
⊢ dist (f^[n] x) (f^[n + 1] x) / (1 - ↑K) ≤ dist x (f x) * ↑K ^ n / (1 - ↑K)

Tactic:
by
      gcongr; exacts [hf.one_sub_K_pos.le, hf.toLipschitzWith.dist_iterate_succ_le_geometric x n]

Goal state after:
Module: Mathlib.Analysis.ODE.DiscreteGronwall

Goal state before:
pp: u b c : ℕ → ℝ
n₀ : ℕ
hun₀ : 0 ≤ u n₀
hu : ∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
hb : ∀ n ≥ n₀, 0 ≤ b n
n : ℕ
hn : n₀ ≤ n
⊢ u n ≤ (u n₀ + ∑ k ∈ Ico n₀ n, b k) * rexp (∑ i ∈ Ico n₀ n, c i)

Tactic:
calc u n
    _ ≤ u n₀ * ∏ i ∈ Ico n₀ n, (1 + c i) +
          ∑ k ∈ Ico n₀ n, b k * ∏ i ∈ Ico (k + 1) n, (1 + c i) :=
        discrete_gronwall_prod_general hu (by grind) hn
    _ ≤ u n₀ * ∏ i ∈ Ico n₀ n, (1 + c i) +
          ∑ k ∈ Ico n₀ n, b k * ∏ i ∈ Ico n₀ n, (1 + c i) := by
        gcongr <;> grind
    _ = (u n₀ + ∑ k ∈ Ico n₀ n, b k) * ∏ i ∈ Ico n₀ n, (1 + c i) := by rw [add_mul, sum_mul]
    _ ≤ (u n₀ + ∑ k ∈ Ico n₀ n, b k) * exp (∑ i ∈ Ico n₀ n, c i) := by
        gcongr <;> try exact add_nonneg hun₀ <| sum_nonneg <| by grind
        simpa [exp_sum] using prod_le_prod (by grind) (by grind [add_one_le_exp])

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case mpr
E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
r L : ℝ≥0
α : C(↑(Icc tmin tmax), E)
⊢ α ∈ {α | LipschitzWith L ⇑α ∧ α t₀ ∈ closedBall x₀ ↑r} → α ∈ range fun α ↦ toContinuousMap α

Tactic:
· rintro ⟨hα1, hα2⟩
    exact ⟨⟨α, hα1, hα2⟩, rfl⟩

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ 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
α : FunSpace t₀ x₀ r L
t : ↑(Icc tmin tmax)
⊢ ContinuousOn (fun t' ↦ f t' (α.compProj t')) (uIcc ↑t₀ ↑t)

Tactic:
apply α.continuousOn_comp_compProj hf |>.mono

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ 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
α : FunSpace t₀ x₀ r L
t : ↑(Icc tmin tmax)
⊢ uIcc ↑t₀ ↑t ⊆ Icc tmin tmax
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case mp
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ 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
⊢ IsFixedPt (next hf hx) α → ∀ (t : ↑(Icc tmin tmax)), α.toFun t = picard f (↑t₀) x α.compProj ↑t

Tactic:
exact fun hα t ↦ congrArg (· t) hα |>.symm

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ 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
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
⊢ |(∫ (x : ℝ) in ↑t₀..↑t, ↑K ^ (n + 1) * |x - ↑t₀| ^ n / ↑n !) * dist α β| ≤
    (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β

Tactic:
intervalIntegral.integral_div,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ 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
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
⊢ |(∫ (x : ℝ) in ↑t₀..↑t, ↑K ^ (n + 1) * |x - ↑t₀| ^ n) / ↑n ! * dist α β| ≤
    (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f ⟨t₀, ⋯⟩ x₀ a r L K
a' r' : ℝ≥0
ha : a' ≤ a
hr : r' < a'
⊢ 0 < ↑a' - ↑r'

Tactic:
simp only [sub_pos, NNReal.coe_lt_coe, hr]

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

Goal state before:
pp: case refine_1
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ eval y P = -0

Tactic:
← neg_eq_iff_eq_neg,

Goal state after:
case refine_1
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ -eval y P = 0
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: case refine_1
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ eval y P = -0

Tactic:
← neg_eq_iff_eq_neg,

Goal state after:
case refine_1
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ -eval y P = 0
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: case refine_1
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ eval y P = -0

Tactic:
← neg_eq_iff_eq_neg,

Goal state after:
case refine_1
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ -eval y P = 0
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: case refine_1
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ eval y P = -0

Tactic:
← neg_eq_iff_eq_neg,

Goal state after:
case refine_1
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ -eval y P = 0
Module: Mathlib.Data.Rat.NatSqrt.Defs

Goal state before:
pp: x prec : ℕ
h : 0 < prec
⊢ x.ratSqrt prec ^ 2 ≤ ↑x

Tactic:
by
  unfold ratSqrt
  rw [div_pow, div_le_iff₀ (by positivity)]
  norm_cast
  exact sqrt_le' (x * prec ^ 2)

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

Goal state before:
pp: case a.refine_2
p : ℂ[X]
this✝¹ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this✝ : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ Integrable ((fun x ↦ x ^ 2) ∘ fun θ ↦ ‖eval (circleMap 0 1 θ) p‖) (volume.restrict (uIoc 0 (2 * π)))

Tactic:
· exact ((continuous_pow 2).comp hcont).integrableOn_Icc.mono_set Set.Ioc_subset_Icc_self

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

Goal state before:
pp: n : ℕ
a : ℝ
h : (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ a ≤ 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n)

Tactic:
rw [mul_comm]

Goal state after:
n : ℕ
a : ℝ
h : (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ a ≤ √(2 - sqrtTwoAddSeries 0 n) * 2 ^ (n + 1)
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: case mp
q : ℚ
hq : 0 ≤ q
y : ℚ
hy : ↑y = √↑q
⊢ ↑q = ↑y * ↑y

Tactic:
hy,

Goal state after:
case mp
q : ℚ
hq : 0 ≤ q
y : ℚ
hy : ↑y = √↑q
⊢ ↑q = √↑q * √↑q
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: q : ℚ
hq : 0 ≤ q
⊢ Irrational √↑q ↔ ¬IsSquare q

Tactic:
by
  refine Iff.not (?_ : Exists _ ↔ Exists _)
  constructor
  · rintro ⟨y, hy⟩
    refine ⟨y, Rat.cast_injective (α := ℝ) ?_⟩
    rw [Rat.cast_mul, hy, mul_self_sqrt (Rat.cast_nonneg.2 hq)]
  · rintro ⟨q', rfl⟩
    exact ⟨|q'|, mod_cast (sqrt_mul_self_eq_abs q').symm⟩

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

Goal state before:
pp: x : ℝ*
r : ℝ
h : 0 ≤ ArchimedeanClass.mk x ∧ stdPart x = r
⊢ x.IsSt r

Tactic:
obtain ⟨h, rfl⟩ := h
    refine fun y hy ↦ ⟨?_, ?_⟩
    · apply lt_of_lt_stdPart coeRingHom h; simpa
    · apply lt_of_stdPart_lt coeRingHom h; simpa

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

Goal state before:
pp: x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -↑r₁ < y ∧ y < ↑r₁)
⊢ 0 < r₁ ∧ ↑r₁ ≤ y

Tactic:
rwa [Classical.not_imp, ← abs_lt, not_lt, abs_of_pos hy₂] at hy₁''

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

Goal state before:
pp: x y : ℝ*
hx : ¬x.Infinitesimal
hp : 0 < x
hy : y.InfiniteNeg
⊢ (x * y).InfiniteNeg

Tactic:
rw [mul_comm]

Goal state after:
x y : ℝ*
hx : ¬x.Infinitesimal
hp : 0 < x
hy : y.InfiniteNeg
⊢ (y * x).InfiniteNeg
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x y : ℝ*
hx : ¬x.Infinitesimal
hy : y.Infinite
⊢ (x * y).Infinite

Tactic:
rw [mul_comm]

Goal state after:
x y : ℝ*
hx : ¬x.Infinitesimal
hy : y.Infinite
⊢ (y * x).Infinite
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * (π / 2) ≤ W k

Tactic:
rw [← le_div_iff₀ pi_div_two_pos, div_eq_inv_mul (W k) _]
  rw [W_eq_integral_sin_pow_div_integral_sin_pow, le_div_iff₀ (integral_sin_pow_pos _)]
  convert! integral_sin_pow_succ_le (2 * k + 1)
  rw [integral_sin_pow (2 * k)]
  simp

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

Goal state before:
pp: x y : ℝ≥0
⊢ Tendsto (fun n ↦ 2⁻¹ ^ n * (dist x y / 2)) atTop (𝓝 (0 * (dist x y / 2)))

Tactic:
exact (_root_.tendsto_pow_atTop_nhds_zero_of_lt_one (by norm_num) (by norm_num)).mul_const _

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

Goal state before:
pp: p : ℝ
⊢ p = 0 ∨ p = 1 → binEntropy p = 0

Tactic:
rintro (rfl | rfl) <;> simp

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hp : p ∈ Ioo 0 1
μ : Measure ℝ
hμ :
  ∀ a ∈ Ici 0,
    IntegrableOn (fun t ↦ cfcₙ ((↑p).rpowIntegrand₀₁ t) a) (Ioi 0) μ ∧
      a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ ((↑p).rpowIntegrand₀₁ t) a ∂μ
h₃' : EqOn (fun a ↦ a ^ p) (fun a ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ ((↑p).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ ((↑p).rpowIntegrand₀₁ t) a ∂μ

Tactic:
refine integral_concaveOn_of_integrand_ae (convex_Ici _) ?_ fun a ha => (hμ a ha).1

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hp : p ∈ Ioo 0 1
μ : Measure ℝ
hμ :
  ∀ a ∈ Ici 0,
    IntegrableOn (fun t ↦ cfcₙ ((↑p).rpowIntegrand₀₁ t) a) (Ioi 0) μ ∧
      a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ ((↑p).rpowIntegrand₀₁ t) a ∂μ
h₃' : EqOn (fun a ↦ a ^ p) (fun a ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ ((↑p).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), ConcaveOn ℝ (Ici 0) (cfcₙ ((↑p).rpowIntegrand₀₁ x))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: case pos
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : q = 0
a b : A
hab : a ≤ b
ha : 0 ≤ a
⊢ (fun a ↦ a ^ ↑0) a ≤ (fun a ↦ a ^ ↑0) b

pp: case neg
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : q = 0
a b : A
hab : a ≤ b
ha : ¬0 ≤ a
⊢ (fun a ↦ a ^ ↑0) a ≤ (fun a ↦ a ^ ↑0) b

Tactic:
· have hb : 0 ≤ b := ha.trans hab
      simp [CFC.rpow_zero a, CFC.rpow_zero b]

Goal state after:
case neg
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : q = 0
a b : A
hab : a ≤ b
ha : ¬0 ≤ a
⊢ (fun a ↦ a ^ ↑0) a ≤ (fun a ↦ a ^ ↑0) b
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
V : E
δ : ℝ
hδ : 0 ≤ δ
h : ∀ x ∈ uIoc a b, ‖f x - V‖ ≤ δ
hsub : uIcc a b ⊆ Ioi 0
hint_f : IntervalIntegrable (fun x ↦ x⁻¹ • f x) volume a b
hint_V : IntervalIntegrable (fun x ↦ x⁻¹ • V) volume a b
hint_inv : IntervalIntegrable (fun x ↦ x⁻¹ * δ) volume a b
x : ℝ
hx : x ∈ uIoc a b
hx_pos : 0 < x
⊢ ‖x⁻¹ • (f x - V)‖ ≤ x⁻¹ * δ

Tactic:
norm_smul,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
V : E
δ : ℝ
hδ : 0 ≤ δ
h : ∀ x ∈ uIoc a b, ‖f x - V‖ ≤ δ
hsub : uIcc a b ⊆ Ioi 0
hint_f : IntervalIntegrable (fun x ↦ x⁻¹ • f x) volume a b
hint_V : IntervalIntegrable (fun x ↦ x⁻¹ • V) volume a b
hint_inv : IntervalIntegrable (fun x ↦ x⁻¹ * δ) volume a b
x : ℝ
hx : x ∈ uIoc a b
hx_pos : 0 < x
⊢ ‖x⁻¹‖ * ‖f x - V‖ ≤ x⁻¹ * δ
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)
u : ℝ → E := fun x ↦ x⁻¹ • f x
hint : ∀ {p q : ℝ}, 0 < p → 0 < q → IntervalIntegrable u volume p q
ε r : ℝ
hε : 0 < ε
hr : 0 < r
⊢ ∫ (x : ℝ) in ε..r, x⁻¹ • (f (a * x) - f (b * x)) =
    (∫ (x : ℝ) in ε..r, x⁻¹ • f (a * x)) - ∫ (x : ℝ) in ε..r, x⁻¹ • f (b * x)

Tactic:
simp_rw [smul_sub]

Goal state after:
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)
u : ℝ → E := fun x ↦ x⁻¹ • f x
hint : ∀ {p q : ℝ}, 0 < p → 0 < q → IntervalIntegrable u volume p q
ε r : ℝ
hε : 0 < ε
hr : 0 < r
⊢ ∫ (x : ℝ) in ε..r, x⁻¹ • f (a * x) - x⁻¹ • f (b * x) =
    (∫ (x : ℝ) in ε..r, x⁻¹ • f (a * x)) - ∫ (x : ℝ) in ε..r, x⁻¹ • f (b * x)
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)
u : ℝ → E := fun x ↦ x⁻¹ • f x
hint : ∀ {p q : ℝ}, 0 < p → 0 < q → IntervalIntegrable u volume p q
hsplit :
  ∀ {ε r : ℝ},
    0 < ε →
      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
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
⊢ Tendsto (fun p ↦ ∫ (x : ℝ) in p.1..p.2, x⁻¹ • (f (a * x) - f (b * x))) (𝓝[>] 0 ×ˢ atTop) (𝓝 (log (b / a) • (L - R)))

Tactic:
rw [tendsto_congr' h_ev, show log (b / a) • (L - R) =
    log (b / a) • L - log (b / a) • R from smul_sub _ _ _]

Goal state after:
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)
u : ℝ → E := fun x ↦ x⁻¹ • f x
hint : ∀ {p q : ℝ}, 0 < p → 0 < q → IntervalIntegrable u volume p q
hsplit :
  ∀ {ε r : ℝ},
    0 < ε →
      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
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
⊢ Tendsto (fun p ↦ (∫ (x : ℝ) in a * p.1..b * p.1, u x) - ∫ (x : ℝ) in a * p.2..b * p.2, u x) (𝓝[>] 0 ×ˢ atTop)
    (𝓝 (log (b / a) • L - log (b / a) • R))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
⊢ x ^ (p - 1) * (t ^ (p - 1) * 1 / (t + 1)) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)

Tactic:
rw [mul_comm]

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm ((algebraMap ℝ A) t, LinearMap.id)
haddl : Function.Injective ⇑addl
hici : Ici 0 = ⇑addl ⁻¹' ⇑addl '' Ici 0
⊢ ⇑addl '' Ici 0 ⊆ {a | IsStrictlyPositive a}

Tactic:
simp only [AffineMap.toConstProdLinearMap_symm_apply, AffineMap.coe_add,
    LinearMap.coe_toAffineMap, LinearMap.id_coe, AffineMap.coe_const, Pi.add_apply, id_eq,
    Function.const_apply, image_add_right, preimage_add_const_Ici, sub_neg_eq_add, zero_add, addl]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm ((algebraMap ℝ A) t, LinearMap.id)
haddl : Function.Injective ⇑addl
hici : Ici 0 = ⇑addl ⁻¹' ⇑addl '' Ici 0
⊢ Ici ((algebraMap ℝ A) t) ⊆ {a | IsStrictlyPositive a}
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
n : ℕ
⊢ s - 1 ≠ -↑n

Tactic:
rcases n with - | m

Goal state after:
case zero
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
⊢ s - 1 ≠ -↑0

case succ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
m : ℕ
⊢ s - 1 ≠ -↑(m + 1)
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
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
⊢ cfcₙ (p.rpowIntegrand₀₁ t) a = t ^ (p - 1) • cfcₙ (p.rpowIntegrand₀₁ 1) (t⁻¹ • a)

Tactic:
have h_mapsTo : MapsTo (t⁻¹ • · : ℝ → ℝ) (Ici 0) (Ici 0) := by
    intro x hx
    simp only [mem_Ici, smul_eq_mul] at hx ⊢
    positivity

Goal state after:
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
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (fun x ↦ t⁻¹ • x) (Ici 0) (Ici 0)
⊢ cfcₙ (p.rpowIntegrand₀₁ t) a = t ^ (p - 1) • cfcₙ (p.rpowIntegrand₀₁ 1) (t⁻¹ • a)
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b : ℝ
⊢ logb (-b) = logb b

Tactic:
ext x; rw [← logb_abs_base b x, ← logb_abs_base (-b) x, abs_neg]

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

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
⊢ clog b r⁻¹ = -log b r

Tactic:
obtain hr | hr := le_total 1 r

Goal state after:
case inl.inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
hr : 1 ≤ r
⊢ clog b r⁻¹ = -log b r

case inl.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
hr : r ≤ 1
⊢ clog b r⁻¹ = -log b r
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 : b ≤ 1
r : R
⊢ clog b r = 0

Tactic:
rw [← neg_log_inv_eq_clog, log_of_left_le_one hb, neg_zero]

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
⊢ 0 ≤ y

Tactic:
hy,

Goal state after:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
⊢ 0 ≤ ε * x * x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case h
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
ha : 1 ≤ a
⊢ b ^ e ≤ a → logb b a ≤ e

Tactic:
rw [logb_le_iff_le_rpow_of_base_lt_one b_pos b_lt_one]

Goal state after:
case h
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
ha : 1 ≤ a
⊢ b ^ e ≤ a → b ^ e ≤ a

case h
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
ha : 1 ≤ a
⊢ 0 < a
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: x : ℝ
⊢ Tendsto (fun ε ↦ ε.mulExpNegMulSq x) (𝓝 0) (𝓝 x)

Tactic:
have : x = (fun ε : ℝ => mulExpNegMulSq ε x) 0 := by
    simp only [mulExpNegMulSq, zero_mul, neg_zero, exp_zero, mul_one]
  nth_rw 2 [this]
  apply Continuous.tendsto (Continuous.mul continuous_const (by fun_prop))

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ᶜ < ε
A : Set α
hA : q A
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K ⊆ A, p K ∧ r < μ K

Tactic:
obtain ⟨K, hK, hK_subset, h_lt⟩ : ∃ K, p K ∧ K ⊆ A ∧ μ (A \ K) < μ A - r := by
    obtain ⟨K', hpK', hK'_lt⟩ := hμ (μ A - r) (tsub_pos_of_lt hr)
    refine ⟨K' ∩ A, hpq K' A hpK' hA, inter_subset_right, ?_⟩
    · refine (measure_mono fun x ↦ ?_).trans_lt hK'_lt
      simp only [sdiff_inter_self_eq_sdiff, mem_sdiff, mem_compl_iff, and_imp, imp_self,
        imp_true_iff]

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 : Set α
hK : p K
hK_subset : K ⊆ A
h_lt : μ (A \ K) < μ A - r
⊢ ∃ K ⊆ A, p K ∧ r < μ K
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsOpenPosMeasure
a✝ : Nontrivial E
U : Set ↑(sphere 0 1)
hUo : IsOpen U
hU : U.Nonempty
⊢ ↑(dim E) ≠ 0

Tactic:
simp [Module.finrank_pos.ne']

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

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

Tactic:
L.weierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice

Goal state after:
case e'_6
L : PeriodPair
⊢ ℘[L] = ℘[L]
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: case refine_2
x : ℝ
hx : 0 < x⁻¹ - 1
⊢ x ∈ range sigmoid

Tactic:
exact ⟨-(log (x⁻¹ - 1)), by simp [sigmoid_def, exp_log hx]⟩

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

Goal state before:
pp: n i : ℕ
hi : i ≤ n
this : 0 < (-1)⁻¹ ^ i * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹
⊢ 0 < (-1) ^ i * leadingCoeffC n i

Tactic:
inv_neg_one

Goal state after:
n i : ℕ
hi : i ≤ n
this : 0 < (-1) ^ i * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹
⊢ 0 < (-1) ^ i * leadingCoeffC n i
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l : ℂ
n : ℕ
⊢ iteratedDeriv n ℘'[L - l] l = ↑(n + 2)! * L.sumInvPow l (n + 3)

Tactic:
have : iteratedDeriv n ℘'[L - l] l / n ! = (↑n + 1) * (↑n + 2) * L.sumInvPow l (n + 3) := by
    simpa using congr($((L.analyticAt_derivWeierstrassPExcept l).hasFPowerSeriesAt
      |>.eq_formalMultilinearSeries (L.hasFPowerSeriesAt_derivWeierstrassPExcept l)).coeff n)
  simp [div_eq_iff, Nat.factorial_ne_zero, Nat.factorial_succ] at this ⊢
  grind

Goal state after: