mathlib-initiative/mathlib-tactics huggingface dataset:
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)
hint : IntegrableOn (fun x ↦ x⁻¹ • (f (a * x) - f (b * x))) (Ioi 0) volume
⊢ ∫ (x : ℝ) in Ioi 0, x⁻¹ • (f (a * x) - f (b * x)) = log (b / a) • (L - R)

Tactic:
by
  have h_lim := (tendsto_intervalIntegral hf ha hb hL hR).mono_left curry_le_prod
  set g := fun x ↦ x⁻¹ • (f (a * x) - f (b * x)) with hg
  apply tendsto_nhds_unique
    (hint.continuousWithinAt_Ici_primitive_Ioi.mono_left (nhdsWithin_mono 0 Ioi_subset_Ici_self))
  rw [tendsto_nhdsWithin_nhds]
  intro ε hε
  rw [Metric.tendsto_nhds] at h_lim
  specialize h_lim (ε / 2) (by positivity)
  rw [eventually_curry_iff, Filter.Eventually, mem_nhdsWithin_iff] at h_lim
  obtain ⟨δ, hδ_pos, hδ⟩ := h_lim
  simp_rw [subset_def, mem_inter_iff, mem_ball] at hδ
  refine ⟨δ, hδ_pos, ?_⟩
  intro x hx hdist
  specialize hδ x ⟨hdist, hx⟩
  rw [mem_ofPred] at hδ
  have hint' : IntegrableOn g (Ioi x) := hint.mono (by grind) (by simp)
  have htends := intervalIntegral_tendsto_integral_Ioi x hint' tendsto_id
  have hle := le_of_tendsto (htends.dist tendsto_const_nhds) (hδ.mono (fun _ hy ↦ hy.le))
  linarith

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

Goal state before:
pp: case hbc
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
⊢ t + 1 ≤ 2 * t

Tactic:
linarith

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

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
⊢ 0 ≤ t

Tactic:
linarith

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

Goal state before:
pp: this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 1 / 2 < 49 / 20 - log 7

Tactic:
lt_sub_iff_add_lt,

Goal state after:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 1 / 2 + log 7 < 49 / 20
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p x : ℝ
hp : 0 < p ∧ p < 1
hx : 0 ≤ x
⊢ -1 < p - 1

Tactic:
linarith

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

Goal state before:
pp: p x : ℝ
hp : 0 < p ∧ p < 1
hx : 0 ≤ x
⊢ p - 2 < -1

Tactic:
linarith

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

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ IntegrableOn (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (Ioi 1) volume

Tactic:
refine ⟨?meas, ?finite⟩
  case meas =>
    refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioi
    exact continuousOn_rpowIntegrand₀₁ hp hx |>.mono (Set.Ioi_subset_Ioi zero_le_one)
  case finite =>
    refine HasFiniteIntegral.mono' (g := fun t => t ^ (p - 2) * x) ?finitebound ?ae_le
    case finitebound =>
      refine HasFiniteIntegral.mul_const ?_ _
      apply Integrable.hasFiniteIntegral
      rw [Set.mem_Ioo] at hp
      refine integrableOn_Ioi_rpow_of_lt ?_ zero_lt_one
      linarith
    case ae_le =>
      refine ae_restrict_of_forall_mem measurableSet_Ioi fun t (ht : 1 < t) => ?_
      rw [Real.norm_of_nonneg (rpowIntegrand₀₁_nonneg hp.1 (by positivity) hx)]
      exact rpowIntegrand₀₁_le_rpow_sub_two_mul_self hp (by positivity) hx

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

Goal state before:
pp: ⊢ StrictAnti eulerMascheroniSeq'

Tactic:
refine strictAnti_nat_of_succ_lt (fun n ↦ ?_)
  rcases Nat.eq_zero_or_pos n with rfl | hn
  · simp [eulerMascheroniSeq']
  simp_rw [eulerMascheroniSeq', eq_false_intro hn.ne', reduceCtorEq, if_false]
  rw [← sub_pos, sub_sub_sub_comm,
    harmonic_succ, Rat.cast_add, ← sub_sub, sub_self, zero_sub, sub_eq_add_neg, neg_sub,
    ← sub_eq_neg_add, sub_pos, ← log_div (by positivity) (by positivity), ← neg_lt_neg_iff,
    ← log_inv]
  refine (log_lt_sub_one_of_pos ?_ ?_).trans_le (le_of_eq ?_)
  · positivity
  · simp [field]
  · simp [field]

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

Goal state before:
pp: case h
m n r : ℕ
hr : 0 < r
⊢ ↑r < ↑r + 1

Tactic:
linarith

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

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

Tactic:
suffices Tendsto (fun n ↦ eulerMascheroniSeq' n - eulerMascheroniSeq n) atTop (𝓝 0) by
    simpa using this.add tendsto_eulerMascheroniSeq
  suffices Tendsto (fun x : ℝ ↦ log (x + 1) - log x) atTop (𝓝 0) by
    apply (this.comp tendsto_natCast_atTop_atTop).congr'
    filter_upwards [eventually_ne_atTop 0] with n hn
    simp [eulerMascheroniSeq, eulerMascheroniSeq', eq_false_intro hn]
  exact tendsto_log_comp_add_sub_log 1

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

Goal state before:
pp: n : ℕ
f : ℝ → ℝ := log ∘ Gamma
this : deriv (fun x ↦ log (Gamma x)) (↑n + 1) = -γ + ↑(harmonic n)
m : ℕ
⊢ ↑n + 1 ≠ -↑m

Tactic:
linarith

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

Goal state before:
pp: n : ℕ
f : ℝ → ℝ := log ∘ Gamma
⊢ deriv Gamma (↑n + 1) = ↑n ! * (-γ + ↑(harmonic n))

Tactic:
suffices deriv (log ∘ Gamma) (n + 1) = -γ + harmonic n by
    rwa [Function.comp_def, deriv.log (differentiableAt_Gamma (fun m ↦ by linarith))
      (by positivity), Gamma_nat_eq_factorial, div_eq_iff_mul_eq (by positivity),
      mul_comm, Eq.comm] at this

Goal state after:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
⊢ deriv (log ∘ Gamma) (↑n + 1) = -γ + ↑(harmonic n)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: n : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
x : ℝ
hx : 0 < x
m : ℕ
⊢ -↑m < x

Tactic:
linarith

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

Goal state before:
pp: p : ℝ
hp : 0 < p ∧ p < 1
⊢ p - 2 < -1

Tactic:
linarith

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

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

Tactic:
linarith

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

Goal state before:
pp: p x : ℝ
hx : 0 ≤ x
hx_zero : x = 0
hp : 0 < p ∧ p < 1
⊢ ?m.78 ≠ 0

Tactic:
linarith

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

Goal state before:
pp: n✝ : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
n : ℕ
hn : 0 < n
⊢ ↑n < ↑n + 1

Tactic:
linarith

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

Goal state before:
pp: n✝ : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
derivLB : ∀ (n : ℕ), 0 < n → log ↑n ≤ deriv f (↑n + 1)
n : ℕ
⊢ ↑n + 1 < ↑n + 2

Tactic:
linarith

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

Goal state before:
pp: n m : ℕ
⊢ ↑n + 1 ≠ -↑m

Tactic:
linarith

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

Goal state before:
pp: b : ℝ
hb : 1 < b
⊢ 0 < b

Tactic:
linarith

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

Goal state before:
pp: b : ℝ
hb : 1 < b
⊢ b ≠ 1

Tactic:
linarith

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

Goal state before:
pp: b x y : ℝ
hb : 1 < b
h : 0 < x
hxy : x ≤ y
⊢ 0 < y

Tactic:
linarith

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

Goal state before:
pp: b : ℝ
b_lt_one : b < 1
⊢ b ≠ 1

Tactic:
linarith

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

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' : x < 1
⊢ 0 < logb b x

Tactic:
by
  rw [logb_pos_iff_of_base_lt_one b_pos b_lt_one hx]
  exact hx'

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

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

Tactic:
linarith

Goal state after:
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 → b ^ e ≤ a

Tactic:
tauto

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

Goal state before:
pp: b x : ℝ
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1

Tactic:
tauto

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
f : X →ᵇ E
⊢ ‖∫ (x : X), f x ∂μ‖ ≤ μ.real Set.univ * ‖f‖

Tactic:
by
  calc  ‖∫ x, f x ∂μ‖
    _ ≤ ∫ x, ‖f x‖ ∂μ := norm_integral_le_integral_norm _
    _ ≤ ∫ _, ‖f‖ ∂μ := ?_
    _ = μ.real Set.univ • ‖f‖ := by rw [integral_const]
  apply integral_mono _ (integrable_const ‖f‖) (fun x ↦ f.norm_coe_le_norm x) -- NOTE: `gcongr`?
  exact (integrable_norm_iff f.continuous.measurable.aestronglyMeasurable).mpr (f.integrable μ)

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

Goal state before:
pp: E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : N ≤ n
hnpos : 0 < ↑n
x : E
⊢ -1 ≤ 0

Tactic:
linarith

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
⊢ -1 < p - 1

Tactic:
linarith

Goal state after:
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✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
s : Set ↑(sphere 0 1)
hs : s ∈ {s | MeasurableSet s}
r : ↑(Ioi 0)
this : Ioo 0 ↑r = ↑r • Ioo 0 1
hpos : 0 < dim E
⊢ μ (Subtype.val '' ⇑(homeomorphUnitSphereProd E) ⁻¹' s ×ˢ Iio r) =
    ↑(dim E) * μ (Ioo 0 1 • Subtype.val '' s) * ENNReal.ofReal (↑r ^ (dim E - 1 + 1) / (↑(dim E - 1) + 1))

Tactic:
toSphere_apply_aux,

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
s : Set ↑(sphere 0 1)
hs : s ∈ {s | MeasurableSet s}
r : ↑(Ioi 0)
this : Ioo 0 ↑r = ↑r • Ioo 0 1
hpos : 0 < dim E
⊢ μ (Ioo 0 ↑r • Subtype.val '' s) =
    ↑(dim E) * μ (Ioo 0 1 • Subtype.val '' s) * ENNReal.ofReal (↑r ^ (dim E - 1 + 1) / (↑(dim E - 1) + 1))
Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral

Goal state before:
pp: case pos
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
hr : 0 < r
⊢ -1 < ↑(Module.finrank ℝ E) - 1 - α

Tactic:
linarith

Goal state after:
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
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
⊢ 0 ≤ 1 - ε / 4

Tactic:
linarith

Goal state after:
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
habs : |1 - ε / 4| = 1 - ε / 4
hy : dist 0 ((1 - ε / 4) • x) < ε / 4
this : 1 - ε / 4 < ε / 4
⊢ False

Tactic:
linarith

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

Goal state before:
pp: r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
h : 2 * r ≤ ‖s‖
⊢ False

Tactic:
linarith

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

Goal state before:
pp: r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this : s ≠ l
⊢ 0 < ‖l‖

Tactic:
linarith

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

Goal state before:
pp: r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ ‖l‖ / 2 ≤ ‖l‖ - ‖s‖

Tactic:
linarith

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

Goal state before:
pp: case pos
n : ℕ
ε : ℝ
h : n ≠ 0 ∧ 0 < ε
⊢ 0 < ↑n * (min ε.toNNReal 2 / 4) ^ n

Tactic:
cases h

Goal state after:
case pos.intro
n : ℕ
ε : ℝ
left✝ : n ≠ 0
right✝ : 0 < ε
⊢ 0 < ↑n * (min ε.toNNReal 2 / 4) ^ n
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case e_a
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ ‖(l + (s - l)) * (l - (s - l))‖ = ‖s * (2 * l - s)‖

Tactic:
simp [← sub_add, two_mul, sub_add_eq_add_sub]

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

Goal state before:
pp: case h₂
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ 2 * ‖l‖ + ‖s‖ ≤ 2.5 * ‖l‖

Tactic:
linarith

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
hl : l₀ ∉ L.lattice
z : ℂ
l : ↥L.lattice
this : ↑l ≠ l₀
⊢ (if ↑l = l₀ then 0 else 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2) = 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2

Tactic:
simp [this]

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
hs : ‖↑l‖ < r
⊢ False

Tactic:
linarith

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
r : ℝ
s : ℂ
hr : 0 < r
hs : ‖s‖ < r
h : 2 * r ≤ 0
h✝ : ¬0 = l₀
this : ¬s = 0
⊢ False

Tactic:
linarith

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 0 ≤ ‖↑l‖ - ‖s‖

Tactic:
linarith

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 0 ≤ 2

Tactic:
linarith

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

Goal state before:
pp: case hab
L : PeriodPair
l₀ : ℂ
r : ℝ
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖l‖
h✝ : ¬↑l = l₀
this✝ : ¬s = ↑l
this : ¬l = 0
hr : r > 0
⊢ ‖l‖ ≤ 2 * (‖l‖ - ‖s‖)

Tactic:
linarith

Goal state after:
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 : ℝ
⊢ IntegrableOn ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) (Ioi 0) volume ↔
    Integrable ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) volume

Tactic:
rw [MeasureTheory.integrableOn_iff_integrable_of_support_subset]
      intro x hx
      simp only [support_indicator, mem_inter_iff, mem_Ioo, Function.mem_support, ne_eq,
        smul_eq_zero, pow_eq_zero_iff', not_or, not_and, Decidable.not_not] at hx
      refine mem_Ioi.mpr hx.1.1

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

Goal state before:
pp: ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left✝¹ : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
KP' : Set E
left✝ : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : P KPᶜ < ENNReal.ofReal ε
hKP' : P' KP'ᶜ < ENNReal.ofReal ε
hKPbound : P (KP ∪ KP')ᶜ < ↑ε.toNNReal
hKP'bound : P' (KP ∪ KP')ᶜ < ↑ε.toNNReal
g' : C(E, ℝ)
hg'approx : ∀ x ∈ KP ∪ KP', ‖g' x - ↑f x‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ) x = g'
g : E →ᵇ ℝ := hg'A.choose
hgA : g ∈ A
hgapprox : ∀ x ∈ K, ‖g x - f x‖ < √ε * const⁻¹
line1 : |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P| < √ε
line3 : |∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P| < √ε
line5 : |∫ (x : E), ε.mulExpNegMulSq (g x) ∂P' - ∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P'| < √ε
line7 : |∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P' - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| < √ε
line2 : |∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P| ≤ √ε
line6 : |∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P' - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P'| ≤ √ε
line4 : |∫ (x : E), ε.mulExpNegMulSq (g x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P'| = 0
⊢ |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P| +
                |∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P| +
              |∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P| +
            |∫ (x : E), ε.mulExpNegMulSq (g x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P'| +
          |∫ (x : E), ε.mulExpNegMulSq (g x) ∂P' - ∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P'| +
        |∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P' - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P'| +
      |∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P' - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| ≤
    6 * √ε

Tactic:
linarith

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

Goal state before:
pp: case zero
L : PeriodPair
l₀ x : ℂ
⊢ (FormalMultilinearSeries.ofScalars ℂ fun i ↦
          if i = 0 then ℘[L - l₀] x
          else (↑i + 1) * (L.sumInvPow x (i + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (i + 2))⁻¹ else 0)).coeff
      0 =
    ∑' (l : ↥L.lattice), if ↑l = l₀ then 0 else (↑0 + 1) * (↑l - x) ^ (-↑(0 + 2)) - Nat.casesOn 0 (↑l ^ (-2)) 0

Tactic:
simp [weierstrassPExcept, sub_sq_comm x, zpow_ofNat]

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

Goal state before:
pp: L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ 2 < i + 3

Tactic:
linarith

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this✝ : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
x : ℝ
hx : x ∈ Ioo a b
this : fderiv ℝ (⇑g) (f x) = g.toContinuousLinearMap
⊢ ‖(fderiv ℝ (⇑g) (f x)) (deriv f x)‖ₑ ≤ ‖deriv f x‖ₑ

Tactic:
simp [this]

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, sin θ = ↑q
a✝¹ : ℚ
a✝ : θ = ↑a✝¹ * π
⊢ θ - π / 2 = (↑a✝¹ - 1 / 2) * π

Tactic:
linarith

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

Goal state before:
pp: n : ℕ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ P.degree < ↑(n + 1)

Tactic:
grw [hP]

Goal state after:
n : ℕ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ ↑n < ↑(n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ P.degree < ↑(n + 1)

Tactic:
grw [hP]

Goal state after:
n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ ↑n < ↑(n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ (∃ k ≤ n, Even k ∧ x = cos (↑k * π / ↑n)) → eval x (T ℝ ↑n) = 1

Tactic:
rintro ⟨k, hk₁, hk₂, hx⟩

Goal state after:
case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hk₁ : k ≤ n
hk₂ : Even k
hx : x = cos (↑k * π / ↑n)
⊢ eval x (T ℝ ↑n) = 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ (∃ k ≤ n, Odd k ∧ x = cos (↑k * π / ↑n)) → eval x (T ℝ ↑n) = -1

Tactic:
rintro ⟨k, hk₁, hk₂, hx⟩

Goal state after:
case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hk₁ : k ≤ n
hk₂ : Odd k
hx : x = cos (↑k * π / ↑n)
⊢ eval x (T ℝ ↑n) = -1
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: k : ℝ
hk : 2 < k
⊢ 1 - k < -1

Tactic:
linarith

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

Goal state before:
pp: R : Type u_1
a b u₀ : R
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ha : 1 < a
h0 : b / (1 - a) < u₀
n : ℕ
h_lt : arithGeom a b u₀ n * (1 - a) < b
⊢ arithGeom a b u₀ n < a * arithGeom a b u₀ n + b

Tactic:
linarith

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

Goal state before:
pp: n : ℤ
k : ℕ
x : ℝ
hx : |x| ≤ 1
hn : 0 ≤ n
⊢ |eval x ((⇑derivative)^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative)^[k] (T ℝ n))

Tactic:
lift n to ℕ using hn

Goal state after:
k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
⊢ |eval x ((⇑derivative)^[k] (T ℝ ↑n))| ≤ eval 1 ((⇑derivative)^[k] (T ℝ ↑n))
Module: Mathlib.Analysis.SpecificLimits.Fibonacci

Goal state before:
pp: ⊢ Tendsto (fun n ↦ ↑(fib (n + 1)) / ↑(fib n)) atTop (𝓝 φ)

Tactic:
have h₁ n : (fib (n + 1) / fib n : ℝ) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n) := by
    simp only [coe_fib_eq, pow_succ, div_pow]
    field
  have h₂ := tendsto_pow_atTop_nhds_zero_of_abs_lt_one (r := ψ / φ) <| by
    rw [abs_div, div_lt_one <| by positivity, abs_of_pos goldenRatio_pos, abs_lt]
    ring_nf
    bound
  rw [show φ = (φ - ψ * 0) / (1 - 0) by ring, funext h₁]
  exact const_sub _ (const_mul _ h₂) |>.div (const_sub _ h₂) <| by simp

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

Goal state before:
pp: ⊢ φ + ψ = 1

Tactic:
rw [goldenRatio, goldenConj]
  ring

Goal state after: