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

Goal state before:
pp: α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
hx : f^[n] x = x
⊢ IsFixedPt f x

Tactic:
have := hf.toLipschitzWith.dist_le_mul x (f x)

Goal state after:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
hx : f^[n] x = x
this : dist (f^[n] x) (f^[n] (f x)) ≤ ↑K * dist x (f x)
⊢ IsFixedPt f x
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case mk.mk
E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
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 :
  ∀ (t : ↑(Icc tmin tmax)),
    { toFun := toFun✝¹, lipschitzWith := lipschitzWith✝¹, mem_closedBall₀ := mem_closedBall₀✝¹ }.toFun t =
      { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ }.toFun t
⊢ { toFun := toFun✝¹, lipschitzWith := lipschitzWith✝¹, mem_closedBall₀ := mem_closedBall₀✝¹ } =
    { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ }

Tactic:
simp only [mk.injEq]

Goal state after:
case mk.mk
E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
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 :
  ∀ (t : ↑(Icc tmin tmax)),
    { toFun := toFun✝¹, lipschitzWith := lipschitzWith✝¹, mem_closedBall₀ := mem_closedBall₀✝¹ }.toFun t =
      { toFun := toFun✝, lipschitzWith := lipschitzWith✝, mem_closedBall₀ := mem_closedBall₀✝ }.toFun t
⊢ toFun✝¹ = toFun✝
Module: Mathlib.Analysis.ODE.Gronwall

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 ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : dist (f a) (g a) ≤ δ
f_bound : ∀ t ∈ Ico a b, dist (v t (f t)) (v t (f t)) ≤ 0
g_bound : ∀ t ∈ Ico a b, dist (v t (g t)) (v t (g t)) ≤ 0
t : ℝ
ht : t ∈ Icc a b
this : dist (f t) (g t) ≤ gronwallBound δ (↑K) (0 + 0) (t - a)
⊢ dist (f t) (g t) ≤ δ * rexp (↑K * (t - a))

Tactic:
rwa [zero_add, gronwallBound_ε0] at this

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x ↦ eval x P / eval x Q) atBot (𝓝 0)
⊢ ¬Q.comp (-X) = 0

Tactic:
comp_eq_zero_iff

Goal state after:
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x ↦ eval x P / eval x Q) atBot (𝓝 0)
⊢ ¬(Q = 0 ∨ eval ((-X).coeff 0) Q = 0 ∧ -X = C ((-X).coeff 0))
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : (Q.comp (-X)).degree < (P.comp (-X)).degree
hQ : Q ≠ 0
⊢ ¬Q.comp (-X) = 0

Tactic:
comp_eq_zero_iff

Goal state after:
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : (Q.comp (-X)).degree < (P.comp (-X)).degree
hQ : Q ≠ 0
⊢ ¬(Q = 0 ∨ eval ((-X).coeff 0) Q = 0 ∧ -X = C ((-X).coeff 0))
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
⊢ ∃ α, α ↑t₀ = x ∧ ∀ t ∈ Icc tmin tmax, α t = picard f (↑t₀) x α t

Tactic:
by
  obtain ⟨α, hα⟩ := FunSpace.exists_isFixedPt_next hf hx
  refine ⟨(FunSpace.next hf hx α).compProj, by simp, fun t ht ↦ ?_⟩
  rw [FunSpace.compProj_apply, FunSpace.next_apply, hα, projIcc_of_mem _ ht]

Goal state after:
Module: Mathlib.Data.Rat.NatSqrt.Defs

Goal state before:
pp: x prec : ℕ
h : 0 < prec
⊢ ↑x * ↑prec ^ 2 < (↑(x * prec ^ 2).sqrt + 1) ^ 2

pp: case h
x prec : ℕ
h : 0 < prec
⊢ ↑prec ≠ 0

pp: case h
x prec : ℕ
h : 0 < prec
⊢ ↑prec ≠ 0

Tactic:
· norm_cast
    exact lt_succ_sqrt' (x * prec ^ 2)

Goal state after:
case h
x prec : ℕ
h : 0 < prec
⊢ ↑prec ≠ 0

case h
x prec : ℕ
h : 0 < prec
⊢ ↑prec ≠ 0
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
P : 1 ≠ 0
C : N.natAbs.Coprime 1
hxr : m * ↑1 ^ n = N ^ n
hv : ¬∃ y, ↑{ num := N, den_nz := P, reduced := C } = ↑y
c1 : ↑↑1 ≠ 0
c2 : ↑↑1 ^ n ≠ 0
hdivn : 1 ∣ N.natAbs
⊢ ↑{ num := N, den_nz := P, reduced := C } = ↑N

Tactic:
rw [mk_eq_divInt, Int.ofNat_one, divInt_one, cast_intCast]

Goal state after:
Module: Mathlib.NumberTheory.Real.Irrational

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

Tactic:
refine Iff.not (?_ : Exists _ ↔ Exists _)

Goal state after:
q : ℚ
hq : 0 ≤ q
⊢ (∃ y, ↑y = √↑q) ↔ ∃ r, q = r * r
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (↑m - x)

Tactic:
by
  simpa only [Rat.cast_intCast] using h.ratCast_sub m

Goal state after:
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x / ↑↑m)

Tactic:
refine h.div_ratCast ?_

Goal state after:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ ↑m ≠ 0
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: f : ℕ → ℝ
hf : Tendsto f atTop atTop
⊢ (ofSeq f).InfinitePos

Tactic:
replace hf := hf.mono_left Nat.hyperfilter_le_atTop
  rw [infinitePos_iff]
  exact ⟨lt_of_tendsto_atTop 0 hf, archimedeanClassMk_neg_of_tendsto_atTop hf⟩

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

Goal state before:
pp: f : ℕ → ℝ
hf : Tendsto f atTop atBot
⊢ (ofSeq f).InfiniteNeg

Tactic:
replace hf := hf.mono_left Nat.hyperfilter_le_atTop
  rw [infiniteNeg_iff]
  exact ⟨lt_of_tendsto_atBot 0 hf, archimedeanClassMk_neg_of_tendsto_atBot hf⟩

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

Goal state before:
pp: x y : ℝ*
⊢ x.InfiniteNeg → ¬y.Infinitesimal → y < 0 → (x * y).InfinitePos

Tactic:
rw [← infinitePos_neg, ← neg_pos, ← neg_mul_neg, ← infinitesimal_neg]

Goal state after:
x y : ℝ*
⊢ (-x).InfinitePos → ¬(-y).Infinitesimal → 0 < -y → (-x * -y).InfinitePos
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: 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 * 1))
⊢ Tendsto (fun k ↦ ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))

Tactic:
rw [mul_one] at abel

Goal state after:
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)
⊢ Tendsto (fun k ↦ ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case succ
x y : ℝ≥0
n : ℕ
ih : dist (x.agmSequences y n).1 (x.agmSequences y n).2 ≤ dist x y / 2 ^ (n + 1)
⊢ dist (x.agmSequences y n).1 (x.agmSequences y n).2 / 2 ≤ dist x y / 2 ^ (n + 1 + 1)

Tactic:
pow_succ,

Goal state after:
case succ
x y : ℝ≥0
n : ℕ
ih : dist (x.agmSequences y n).1 (x.agmSequences y n).2 ≤ dist x y / 2 ^ (n + 1)
⊢ dist (x.agmSequences y n).1 (x.agmSequences y n).2 / 2 ≤ dist x y / (2 ^ (n + 1) * 2)
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
⊢ Tendsto (fun n ↦ (x.agmSequences y n).1) atTop (𝓝 (x.agm y))

Tactic:
rw [agm_eq_ciSup]
  exact tendsto_atTop_ciSup agmSequences_fst_monotone bddAbove_range_agmSequences_fst

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto

Goal state before:
pp: case e_a.e_a.e_a
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ x ^ p = rexp (log x * p)

Tactic:
Real.exp_mul,

Goal state after:
case e_a.e_a.e_a
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ x ^ p = rexp (log x) ^ p
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
F : Filter ℝ
hpos : ∀ᶠ (t : ℝ) in F, 0 < t
V : E
huni : ∀ δ > 0, ∀ᶠ (t : ℝ) in F, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ
δ : ℝ
⊢ δ > 0 → ∀ᶠ (x : ℝ) in F, dist (∫ (x : ℝ) in a * x..b * x, x⁻¹ • f x) (log (b / a) • V) < δ

Tactic:
hδ

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
F : Filter ℝ
hpos : ∀ᶠ (t : ℝ) in F, 0 < t
V : E
huni : ∀ δ > 0, ∀ᶠ (t : ℝ) in F, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ
δ : ℝ
hδ : δ > 0
⊢ ∀ᶠ (x : ℝ) in F, dist (∫ (x : ℝ) in a * x..b * x, x⁻¹ • f x) (log (b / a) • V) < δ
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
δ : ℝ
⊢ δ > 0 → ∀ᶠ (t : ℝ) in 𝓝[{x | (fun t ↦ 0 < t) x}] 0, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - L‖ ≤ δ

Tactic:
hδ

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
δ : ℝ
hδ : δ > 0
⊢ ∀ᶠ (t : ℝ) in 𝓝[{x | (fun t ↦ 0 < t) x}] 0, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - L‖ ≤ δ
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hR : Tendsto f atTop (𝓝 R)
δ : ℝ
⊢ δ > 0 → ∀ᶠ (t : ℝ) in atTop, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - R‖ ≤ δ

Tactic:
hδ

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hR : Tendsto f atTop (𝓝 R)
δ : ℝ
hδ : δ > 0
⊢ ∀ᶠ (t : ℝ) in atTop, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - 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 * t) ^ (p - 1) * x / (x * t + x) = x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x)))

Tactic:
rw [← mul_assoc, mul_div_assoc, Real.mul_rpow hx ht]

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

Goal state before:
pp: ⊢ Gammaℂ 1 = 1 / ↑π

Tactic:
rw [Gammaℂ_def, cpow_neg_one, Complex.Gamma_one]
  ring

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

Goal state before:
pp: case inr
n : ℕ
hn : n > 0
⊢ (if n + 1 = 0 then 2 else ↑(harmonic (n + 1)) - log ↑(n + 1)) < if n = 0 then 2 else ↑(harmonic n) - log ↑n

Tactic:
eq_false_intro hn.ne',

Goal state after:
case inr
n : ℕ
hn : n > 0
⊢ (if n + 1 = 0 then 2 else ↑(harmonic (n + 1)) - log ↑(n + 1)) < if False then 2 else ↑(harmonic n) - log ↑n
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ HasFiniteIntegral (fun t ↦ t ^ (p - 2) * x) (volume.restrict (Ioi 1))

Tactic:
refine HasFiniteIntegral.mul_const ?_ _

Goal state after:
p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ HasFiniteIntegral (fun t ↦ t ^ (p - 2)) (volume.restrict (Ioi 1))
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: m n : ℕ
⊢ eulerMascheroniSeq m < eulerMascheroniSeq' n

Tactic:
by
  have (r : ℕ) : eulerMascheroniSeq r < eulerMascheroniSeq' r := by
    rcases eq_zero_or_pos r with rfl | hr
    · simp [eulerMascheroniSeq, eulerMascheroniSeq']
    simp only [eulerMascheroniSeq, eulerMascheroniSeq', hr.ne', if_false]
    gcongr
    linarith
  apply (strictMono_eulerMascheroniSeq.monotone (le_max_left m n)).trans_lt
  exact (this _).trans_le (strictAnti_eulerMascheroniSeq'.antitone (le_max_right m n))

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

Goal state before:
pp: ⊢ Tendsto eulerMascheroniSeq atTop (𝓝 eulerMascheroniConstant)

Tactic:
by
  have := tendsto_atTop_ciSup strictMono_eulerMascheroniSeq.monotone ?_
  · rwa [eulerMascheroniConstant, this.limUnder_eq]
  · exact ⟨_, fun _ ⟨_, hn⟩ ↦ hn ▸ (eulerMascheroniSeq_lt_eulerMascheroniSeq' _ 1).le⟩

Goal state after:
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)) (1 / 2) + deriv (fun s ↦ 2 ^ (1 - 2 * s)) (1 / 2) + γ) =
    √π * (-2 * γ + deriv (fun s ↦ 2 ^ (1 - 2 * s)) (1 / 2) + γ)

Tactic:
by
    congr 3
    change deriv (Gamma ∘ fun s ↦ 2 * s) _ = _
    rw [deriv_comp, deriv_const_mul_id, mul_one_div, div_self two_ne_zero]
    · rw [mul_comm, hasDerivAt_Gamma_one.deriv, mul_neg, neg_mul]
    · apply h_diff; simp -- s = 1
    · fun_prop

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone

Goal state before:
pp: x : ℝ
hex : x ∈ Ici (rexp 1)
y : ℝ
hey : y ∈ Ici (rexp 1)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
hyx : 0 ≤ y / x - 1
⊢ (fun x ↦ log x / x) y ≤ (fun x ↦ log x / x) x

Tactic:
rw [div_le_iff₀ y_pos, ← sub_le_sub_iff_right (log x)]

Goal state after:
x : ℝ
hex : x ∈ Ici (rexp 1)
y : ℝ
hey : y ∈ Ici (rexp 1)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
hyx : 0 ≤ y / x - 1
⊢ log y - log x ≤ (fun x ↦ log x / x) x * y - log x
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:

Tactic:
∫⁻ x, ‖f x‖₊ ∂μ
    _ ≤ ‖f‖₊ * (μ Set.univ) := f.lintegral_nnnorm_le μ
    _ < ∞                   := ENNReal.mul_lt_top ENNReal.coe_lt_top (measure_lt_top μ Set.univ)

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))

Tactic:
have one_lt_p : -1 < p - 1 := by linarith
  have obs : ∀ x : ℝ, ∫ t : ℝ in 0..x, t ^ (p - 1) = x ^ p / p := by
    intro x
    rw [integral_rpow (Or.inl one_lt_p)]
    simp [Real.zero_rpow p_pos.ne.symm]
  set g := fun t : ℝ => t ^ (p - 1)
  have g_nn : ∀ᵐ t ∂volume.restrict (Ioi (0 : ℝ)), 0 ≤ g t := by
    filter_upwards [self_mem_ae_restrict (measurableSet_Ioi : MeasurableSet (Ioi (0 : ℝ)))]
    intro t t_pos
    exact Real.rpow_nonneg (mem_Ioi.mp t_pos).le (p - 1)
  have g_intble (t) (ht : 0 < t) : IntervalIntegrable g volume 0 t :=
    intervalIntegral.intervalIntegrable_rpow' one_lt_p
  have key := lintegral_comp_eq_lintegral_meas_le_mul μ f_nn f_mble g_intble g_nn
  rw [← key, ← lintegral_const_mul'' (ENNReal.ofReal p)] <;> simp_rw [obs]
  · congr with ω
    rw [← ENNReal.ofReal_mul p_pos.le, mul_div_cancel₀ (f ω ^ p) p_pos.ne.symm]
  · have aux := (measurable_const (a := p)).aemeasurable (μ := μ)
    exact measurable_id.ennreal_ofReal.comp_aemeasurable <| (f_mble.pow aux).div_const p

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

Goal state before:
pp: n a fuel : ℕ
ih : ∀ {guess : ℕ}, a < (guess + 1) ^ (n + 2) → a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
h : (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
⊢ a < (go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2)) + 1) ^ (n + 2)

Tactic:
rcases eq_or_ne guess 0 with rfl | hguess

Goal state after:
case inl
n a fuel : ℕ
ih : ∀ {guess : ℕ}, a < (guess + 1) ^ (n + 2) → a < (go n a fuel guess + 1) ^ (n + 2)
hlt : a < (0 + 1) ^ (n + 2)
h : (a / 0 ^ (n + 1) + (n + 1) * 0) / (n + 2) < 0
⊢ a < (go n a fuel ((a / 0 ^ (n + 1) + (n + 1) * 0) / (n + 2)) + 1) ^ (n + 2)

case inr
n a fuel : ℕ
ih : ∀ {guess : ℕ}, a < (guess + 1) ^ (n + 2) → a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
h : (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
hguess : guess ≠ 0
⊢ a < (go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2)) + 1) ^ (n + 2)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ DifferentiableOn ℂ ℘[L] (↑L.lattice)ᶜ

Tactic:
← L.weierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice

Goal state after:
L : PeriodPair
⊢ DifferentiableOn ℂ ℘[L - L.ω₁ / 2] (↑L.lattice)ᶜ
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
⊢ 0 < stirlingSeq (n + 1)

Tactic:
unfold stirlingSeq; positivity

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

Goal state before:
pp: n m : ℤ
⊢ ∫ (x : ℝ), eval x (T ℝ n) * eval x (T ℝ m) ∂measureT =
    (∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT) / 2

Tactic:
by
  suffices ∫ x, (2 * T ℝ n * T ℝ m).eval x ∂measureT =
      (∫ x, (T ℝ (n + m)).eval x ∂measureT) +
      (∫ x, (T ℝ (n - m)).eval x ∂measureT) by
    simp_rw [eval_mul, eval_ofNat, mul_assoc] at this
    rw [MeasureTheory.integral_const_mul] at this
    grind
  simp_rw [T_mul_T, eval_add]
  rw [MeasureTheory.integral_add
    (integrable_measureT (by fun_prop)) (integrable_measureT (by fun_prop))]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: n : ℕ
x✝ : n + 1 ≠ 0
⊢ #(box (n + 1)) = 8 * (n + 1)

Tactic:
Prod.card_box_succ,

Goal state after:
n : ℕ
x✝ : n + 1 ≠ 0
⊢ #(Icc (-↑n.succ) ↑n.succ) * #(Icc (-↑n.succ) ↑n.succ) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n) = 8 * (n + 1)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
⊢ r1 z ≤ (c * z.re + d) ^ 2 + (c * z.im) ^ 2

Tactic:
have H1 : (c * z.re + d) ^ 2 + (c * z.im) ^ 2 =
    c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2 := by ring

Goal state after:
z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
H1 : (c * z.re + d) ^ 2 + (c * z.im) ^ 2 = c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2
⊢ r1 z ≤ (c * z.re + d) ^ 2 + (c * z.im) ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℤ
x : ℝ
hx : x ≤ -1
⊢ 1 ≤ ↑↑n.negOnePow * eval x (T ℝ n)

Tactic:
rw [← neg_neg x, T_eval_neg]

Goal state after:
n : ℤ
x : ℝ
hx : x ≤ -1
⊢ 1 ≤ ↑↑n.negOnePow * (↑↑n.negOnePow * eval (-x) (T ℝ n))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℤ
hn : n ≠ 0
x : ℝ
hx : x < -1
⊢ 1 < ↑↑n.negOnePow * eval x (T ℝ n)

Tactic:
rw [← neg_neg x, T_eval_neg]

Goal state after:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : x < -1
⊢ 1 < ↑↑n.negOnePow * (↑↑n.negOnePow * eval (-x) (T ℝ n))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z x : ℂ
hx : ∀ (l : ↥L.lattice), ‖z - x‖ < ‖↑l - x‖
⊢ HasSum (fun i ↦ (L.weierstrassPExceptSeries (L.ω₁ / 2) x).coeff i * (z - x) ^ i) (℘[L] z)

Tactic:
← L.weierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice

Goal state after:
L : PeriodPair
z x : ℂ
hx : ∀ (l : ↥L.lattice), ‖z - x‖ < ‖↑l - x‖
⊢ HasSum (fun i ↦ (L.weierstrassPExceptSeries (L.ω₁ / 2) x).coeff i * (z - x) ^ i) (℘[L - L.ω₁ / 2] z)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice)ᶜ
⊢ HasFPowerSeriesOnBall ℘[L] (L.weierstrassPExceptSeries (L.ω₁ / 2) x) x ↑r

Tactic:
← L.weierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice

Goal state after:
L : PeriodPair
x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice)ᶜ
⊢ HasFPowerSeriesOnBall ℘[L - L.ω₁ / 2] (L.weierstrassPExceptSeries (L.ω₁ / 2) x) x ↑r
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: case refine_2
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n ↦ u n / ↑n)
L : ℝ
hL : L > h.lim
⊢ ∀ᶠ (b : ℕ) in atTop, u b / ↑b < L

Tactic:
obtain ⟨n, npos, hn⟩ : ∃ n : ℕ, 0 < n ∧ u n / n < L := by
      rw [Subadditive.lim] at hL
      rcases exists_lt_of_csInf_lt (by simp) hL with ⟨x, hx, xL⟩
      rcases (mem_image _ _ _).1 hx with ⟨n, hn, rfl⟩
      exact ⟨n, zero_lt_one.trans_le hn, xL⟩

Goal state after:
case refine_2
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n ↦ u n / ↑n)
L : ℝ
hL : L > h.lim
n : ℕ
npos : 0 < n
hn : u n / ↑n < L
⊢ ∀ᶠ (b : ℕ) in atTop, u b / ↑b < L
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type v
inst✝³ : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝² : Abelian C
inst✝¹ : IsGrothendieckAbelian.{v, v, u} C
inst✝ : Nonempty D
⊢ IsSeparator (projectiveSeparator C)

Tactic:
exact isSeparator_projectiveSeparator

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
⊢ ∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, 1 / (c ^ i) ^ 2 = ∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, (c⁻¹ ^ 2) ^ i

Tactic:
simp [← pow_mul, mul_comm]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I J : InjectiveResolution X
⊢ I.ι ≫ (I.homotopyEquiv J).hom = J.ι

Tactic:
simp [homotopyEquiv]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I J : InjectiveResolution X
⊢ J.ι ≫ (I.homotopyEquiv J).inv = I.ι

Tactic:
simp [homotopyEquiv]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
⊢ ∃ a, pseudoApply S.f a = ⟦b⟧

Tactic:
obtain ⟨c, hc⟩ := KernelFork.IsLimit.lift' hS.isLimitImage _ hb'

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ ∃ a, pseudoApply S.f a = ⟦b⟧
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
R : ProjectiveResolution X
n✝ : ℕ
inst✝ : HasDerivedCategory C
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
⊢ R.cochainComplex.d (-↑m) (-↑n) ≫ (R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f = 0

Tactic:
by simpa [cochainComplex_d _ _ _ _ _ rfl rfl]

Goal state after: