mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.Reproducing

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝⁷ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : RKHS 𝕜 H X V
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace V
s : X →₀ V →L[𝕜] V
⊢ IsSelfAdjoint ((s.sum fun i xi ↦ s.sum fun j xj ↦ star xi * kernel H i j * xj) - 0)

Tactic:
rw [IsSelfAdjoint, sub_zero, star_finsuppSum, Finsupp.sum_comm]

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝⁷ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : RKHS 𝕜 H X V
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace V
s : X →₀ V →L[𝕜] V
⊢ (s.sum fun i m ↦ star (fun i xi ↦ s.sum fun j xj ↦ star xi * kernel H i j * xj) i m) =
    s.sum fun x' v' ↦ s.sum fun x v ↦ star v * kernel H x x' * v'
Module: Mathlib.Analysis.InnerProductSpace.Trace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype ι
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
i : ι
⊢ (b.toBasis.repr (T (b i))) i = ⟪b i, T (b i)⟫_𝕜

Tactic:
b.coe_toBasis_repr_apply,

Goal state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype ι
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
i : ι
⊢ (b.repr (T (b i))).ofLp i = ⟪b i, T (b i)⟫_𝕜
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
this : ∀ {r : 𝕜} (s : Set E), μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s
⊢ μH[d] s ≤ ↑(‖r⁻¹‖₊ ^ d) * μH[d] (r • s)

Tactic:
refine Eq.trans_le ?_ (this (r • s))

Goal state after:
𝕜 : Type u_4
E : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
this : ∀ {r : 𝕜} (s : Set E), μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s
⊢ μH[d] s = μH[d] (r⁻¹ • r • s)
Module: Mathlib.Analysis.InnerProductSpace.Reproducing

Goal state before:
pp: case zero
𝕜 : Type u_1
inst✝⁸ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : RKHS 𝕜 H X V
inst✝² : CompleteSpace H
inst✝¹ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
inst✝ : Fact K.PosSemidef
f : OfKernel K
h : (ContinuousLinearMap.pi fun x ↦ adjoint (kerFun K x)) f = 0
⊢ ⟪↑0, f⟫_𝕜 = 0

Tactic:
have : @UniformSpace.Completion.coe' (H₀ K) PseudoMetricSpace.toUniformSpace 0 = 0 := rfl
      simp [this]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
α : Type u_4
l : Filter α
f : α → E →WOT[𝕜] F
A : E →WOT[𝕜] F
⊢ (∀ (x : E) (y : StrongDual 𝕜 F), Tendsto (fun a ↦ y ((f a) x)) l (𝓝 (y (A x)))) ↔
    ∀ (x : E) (y : F), Tendsto (fun a ↦ ⟪y, (f a) x⟫_𝕜) l (𝓝 ⟪y, A x⟫_𝕜)

Tactic:
exact .symm <| forall_congr' fun _ ↦
    Equiv.forall_congr (InnerProductSpace.toDual 𝕜 F) fun _ ↦ Iff.rfl

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹⁰ : EMetricSpace X
inst✝⁹ : EMetricSpace Y
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
K : Set E
hK : IsCompact K
⊢ μH[↑(finrank ℝ E)] K < ∞

Tactic:
set e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq (by simp)

Goal state after:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹⁰ : EMetricSpace X
inst✝⁹ : EMetricSpace Y
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
K : Set E
hK : IsCompact K
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
⊢ μH[↑(finrank ℝ E)] K < ∞
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹⁰ : EMetricSpace X
inst✝⁹ : EMetricSpace Y
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
⊢ μH[↑(finrank ℝ E)] U ≠ 0

Tactic:
set e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq (by simp)

Goal state after:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹⁰ : EMetricSpace X
inst✝⁹ : EMetricSpace Y
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
⊢ μH[↑(finrank ℝ E)] U ≠ 0
Module: Mathlib.Analysis.LocallyConvex.WeakSpace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
⊢ ⇑(toWeakSpace 𝕜 E) '' (closedConvexHull 𝕜) s = (closedConvexHull 𝕜) (⇑(toWeakSpace 𝕜 E) '' s)

Tactic:
by
  rw [closedConvexHull_eq_closure_convexHull (𝕜 := 𝕜),
    ((convex_convexHull 𝕜 s).lift ℝ).toWeakSpace_closure _, closedConvexHull_eq_closure_convexHull]
  congr
  refine LinearMap.image_convexHull (toWeakSpace 𝕜 E).toLinearMap s

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WeakSpace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E →ₗ[𝕜] F
he : ∀ (f : StrongDual 𝕜 F), Continuous ⇑(e.dualMap ↑f)
⊢ ⇑e '' closure s ⊆ closure (⇑e '' s)

Tactic:
suffices he' : Continuous (toWeakSpace 𝕜 F <| e <| (toWeakSpace 𝕜 E).symm ·) by
    have h_convex : Convex ℝ (e '' s) := hs.linear_image (F := F) e
    rw [← Set.image_subset_image_iff (toWeakSpace 𝕜 F).injective, h_convex.toWeakSpace_closure 𝕜]
    simpa only [Set.image_image, ← hs.toWeakSpace_closure 𝕜, LinearEquiv.symm_apply_apply]
      using he'.continuousOn.image_closure (s := toWeakSpace 𝕜 E '' s)
  exact WeakBilin.continuous_of_continuous_eval _ fun f ↦ WeakBilin.eval_continuous _ ({
      toLinearMap := e.dualMap f
      cont := by dsimp; fun_prop } : StrongDual 𝕜 E)

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (⟪x, a⟫ + ((o.areaForm x) a * 0 - 0 * 1)) * (⟪a, y⟫ + ((o.areaForm a) y * 0 - 0 * 1)) -
      (0 + ((o.areaForm x) a * 1 + 0 * 0)) * (0 + ((o.areaForm a) y * 1 + 0 * 0)) =
    ‖a‖ ^ 2 * (⟪x, y⟫ + ((o.areaForm x) y * 0 - 0 * 1)) - 0 * (0 + ((o.areaForm x) y * 1 + 0 * 0))

Tactic:
rw [real_inner_comm a x, o.areaForm_swap x a]

Goal state after:
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (⟪a, x⟫ + (-(o.areaForm a) x * 0 - 0 * 1)) * (⟪a, y⟫ + ((o.areaForm a) y * 0 - 0 * 1)) -
      (0 + (-(o.areaForm a) x * 1 + 0 * 0)) * (0 + ((o.areaForm a) y * 1 + 0 * 0)) =
    ‖a‖ ^ 2 * (⟪x, y⟫ + ((o.areaForm x) y * 0 - 0 * 1)) - 0 * (0 + ((o.areaForm x) y * 1 + 0 * 0))
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (⟪x, a⟫ + ((o.areaForm x) a * 0 - 0 * 1)) * (0 + ((o.areaForm a) y * 1 + 0 * 0)) +
      (0 + ((o.areaForm x) a * 1 + 0 * 0)) * (⟪a, y⟫ + ((o.areaForm a) y * 0 - 0 * 1)) =
    ‖a‖ ^ 2 * (0 + ((o.areaForm x) y * 1 + 0 * 0)) + 0 * (⟪x, y⟫ + ((o.areaForm x) y * 0 - 0 * 1))

Tactic:
rw [real_inner_comm a x, o.areaForm_swap x a]

Goal state after:
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (⟪a, x⟫ + (-(o.areaForm a) x * 0 - 0 * 1)) * (0 + ((o.areaForm a) y * 1 + 0 * 0)) +
      (0 + (-(o.areaForm a) x * 1 + 0 * 0)) * (⟪a, y⟫ + ((o.areaForm a) y * 0 - 0 * 1)) =
    ‖a‖ ^ 2 * (0 + ((o.areaForm x) y * 1 + 0 * 0)) + 0 * (⟪x, y⟫ + ((o.areaForm x) y * 0 - 0 * 1))
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: ⊢ rexp ∘ Neg.neg '' univ = Ioi 0

Tactic:
rw [Set.image_comp, Set.image_univ_of_surjective neg_surjective, Set.image_univ, Real.range_exp]

Goal state after:
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
h2π : 2 * π ≠ 0
⊢ Integrable (𝓕 fun u ↦ rexp (-(σ * u)) • f (rexp (-u))) volume

Tactic:
simpa [mellin_eq_fourier, mul_div_cancel_right₀ _ h2π] using hFf.comp_mul_right' h2π

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

Goal state before:
pp: s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
⊢ MemLp (fun x ↦ ‖f c u x‖ ^ (ENNReal.ofReal (1 / c)).toReal) (ENNReal.ofReal (1 / c) / ENNReal.ofReal (1 / c))
    (volume.restrict (Ioi 0))

pp: s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
⊢ AEStronglyMeasurable (f c u) (volume.restrict (Ioi 0))

Tactic:
ENNReal.toReal_ofReal (one_div_nonneg.mpr hc.le),

Goal state after:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
⊢ MemLp (fun x ↦ ‖f c u x‖ ^ (1 / c)) (ENNReal.ofReal (1 / c) / ENNReal.ofReal (1 / c)) (volume.restrict (Ioi 0))

s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
⊢ AEStronglyMeasurable (f c u) (volume.restrict (Ioi 0))
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun x ↦ ↑x * ↑(g x)) atTop (𝓝 ↑t)
x : ℝ
hg1 : -1 ≤ g x
⊢ ↑x * Complex.log (1 + ↑(g x)) = ↑x * Complex.log ↑(1 + g x)

Tactic:
Complex.ofReal_add,

Goal state after:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun x ↦ ↑x * ↑(g x)) atTop (𝓝 ↑t)
x : ℝ
hg1 : -1 ≤ g x
⊢ ↑x * Complex.log (1 + ↑(g x)) = ↑x * Complex.log (↑1 + ↑(g x))
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun x ↦ ↑x * ↑(g x)) atTop (𝓝 ↑t)
x : ℝ
hg1 : -1 ≤ g x
⊢ (1 + ↑(g x)) ^ ↑x = ↑(1 + g x) ^ ↑x

Tactic:
Complex.ofReal_add,

Goal state after:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun x ↦ ↑x * ↑(g x)) atTop (𝓝 ↑t)
x : ℝ
hg1 : -1 ≤ g x
⊢ (1 + ↑(g x)) ^ ↑x = (↑1 + ↑(g x)) ^ ↑x
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case hbc.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
hs_bot : b < s.re
F : ℂ → ℝ → E := fun z t ↦ ↑t ^ (z - 1) • f t
F' : ℂ → ℝ → E := fun z t ↦ (↑t ^ (z - 1) * ↑(log t)) • f t
v : ℝ
hv0 : 0 < v
hv1 : v < s.re - b
hv2 : v < a - s.re
bound : ℝ → ℝ := fun t ↦ (t ^ (s.re + v - 1) + t ^ (s.re - v - 1)) * |log t| * ‖f t‖
h1 : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) (volume.restrict (Ioi 0))
h2 : IntegrableOn (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (F' s) (volume.restrict (Ioi 0))
t : ℝ
ht : t ∈ Ioi 0
z : ℂ
hz : ‖s - z‖ < v
h : t < 1
hz' : (s - z).re ≤ v
⊢ s.re - v ≤ z.re

Tactic:
rwa [sub_re, sub_le_iff_le_add, ← sub_le_iff_le_add'] at hz'

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

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
hx : 0 < x
hx' : x ≤ 1
hn' : 0 < ↑n
this : f ↑n + x * log ↑n = (1 - x) * f ↑n + x * f (↑n + 1)
⊢ f (↑n + x) ≤ f ↑n + x * log ↑n

Tactic:
rw [this, (by ring : (n : ℝ) + x = (1 - x) * n + x * (n + 1))]

Goal state after:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
hx : 0 < x
hx' : x ≤ 1
hn' : 0 < ↑n
this : f ↑n + x * log ↑n = (1 - x) * f ↑n + x * f (↑n + 1)
⊢ f ((1 - x) * ↑n + x * (↑n + 1)) ≤ (1 - x) * f ↑n + x * f (↑n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case refine_1.inl
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
this : ∀ (m : ℕ), ↑m < x → x ≤ ↑m + 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
h✝ : x < 1
⊢ ↑⌈x - 1⌉₊ < x

Tactic:
rwa [Nat.ceil_eq_zero.mpr (by linarith : x - 1 ≤ 0), Nat.cast_zero]

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

Goal state before:
pp: case e'_6
⊢ Ioi 0 ∩ Ici 2 = Ici 2

Tactic:
rw [inter_eq_right]

Goal state after:
case e'_6
⊢ Ici 2 ⊆ Ioi 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: ⊢ √π / √π = 1

Tactic:
div_self (sqrt_ne_zero'.mpr pi_pos)

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
hs : Bornology.IsBounded s
⊢ asymptoticCone ℝ s ⊆ {0}

Tactic:
by
  intro v h
  by_contra! hv
  exact h (asymptoticNhds_le_cobounded hv hs)

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
n : ℕ
⊢ s.GammaSeq n = ↑n ^ s * s.betaIntegral (↑n + 1)

Tactic:
by
  rw [GammaSeq, betaIntegral_eval_nat_add_one_right hs n, ← mul_div_assoc]

Goal state after:
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : AffineSubspace k P
hs : (↑s).Nonempty
p : P
hp : p ∈ ↑s
v : V
⊢ v ∈ asymptoticCone k ↑s ↔ v ∈ closure[inst✝⁵] ↑s.direction

Tactic:
simp_rw [← asymptoticCone_submodule, mem_asymptoticCone_iff, ← asymptoticNhds_vadd_pure v p,
    vadd_pure, frequently_map, SetLike.mem_coe, s.vadd_mem_iff_mem_direction _ hp]

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

Goal state before:
pp: case pos
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : s.im = 0
this : s = ↑s.re
n : ℕ
⊢ s.re ≠ -↑n

Tactic:
specialize hs n

Goal state after:
case pos
s : ℂ
h_im : s.im = 0
this : s = ↑s.re
n : ℕ
hs : s ≠ -↑n
⊢ s.re ≠ -↑n
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case e'_3.e'_4
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : ¬i = 1
x : P ≃ᵢ P
hx : s.points ∘ ⇑(Equiv.trans (Equiv.swap 0 i) (Equiv.swap 1 j)) = ⇑x ∘ s.points
⊢ (Equiv.swap 1 j) ((Equiv.swap 0 i) 1) = j

Tactic:
Equiv.swap_apply_of_ne_of_ne (by simp [hn]) (Ne.symm hi)

Goal state after:
case e'_3.e'_4
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : ¬i = 1
x : P ≃ᵢ P
hx : s.points ∘ ⇑(Equiv.trans (Equiv.swap 0 i) (Equiv.swap 1 j)) = ⇑x ∘ s.points
⊢ (Equiv.swap 1 j) 1 = j
Module: Mathlib.Analysis.Normed.Ring.Ultra

Goal state before:
pp: R : Type u_1
inst✝² : SeminormedRing R
inst✝¹ : NormOneClass R
inst✝ : IsUltrametricDist R
z : ℤ
⊢ ‖↑z‖₊ ≤ 1

Tactic:
by
  cases z <;>
  simpa only [Int.ofNat_eq_natCast, Int.cast_natCast, Int.cast_negSucc, Nat.cast_one, nnnorm_neg]
    using nnnorm_natCast_le_one _ _

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
⊢ x ≠ 0

Tactic:
simpa using H.trans' zero_lt_one

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
a : ℝ
ha : max 1 ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : (m + 1) • max 1 ‖x‖ ^ m < a ^ m
⊢ 1 ∈ {x | 0 ≤ x}

Tactic:
by simp [zero_le_one]

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (n : ℕ), ‖↑n‖ ≤ 1
⊢ IsUltrametricDist R

Tactic:
refine isUltrametricDist_of_forall_pow_norm_le_nsmul_pow_max_one_norm (fun x m ↦ ?_)
  -- we first use our hypothesis about the norm of naturals to have that multiplication by
  -- naturals keeps the norm small
  replace h (x : R) (n : ℕ) : ‖n • x‖ ≤ ‖x‖ := by
    rw [nsmul_eq_mul, norm_mul]
    rcases (norm_nonneg x).eq_or_lt with hx | hx
    · simp only [← hx, mul_zero, le_refl]
    · simpa only [mul_le_iff_le_one_left hx] using h _
  -- we expand the LHS using the binomial theorem, and apply the hypothesis to bound each term by
  -- a power of ‖x‖
  transitivity ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k
  · simpa only [← norm_pow, (Commute.one_right x).add_pow, one_pow, mul_one, nsmul_eq_mul,
      Nat.cast_comm] using (norm_sum_le _ _).trans (Finset.sum_le_sum fun _ _ ↦ h _ _)
  -- the nature of the norm means that one of `1` and `‖x‖ ^ m` is the largest of the two, so the
  -- other terms in the binomial expansion are bounded by the max of these, and the number of terms
  -- in the sum is precisely `m + 1`
  rw [← Finset.card_range (m + 1), ← Finset.sum_const, Finset.card_range]
  rcases max_cases 1 (‖x‖ ^ m) with (⟨hm, hx⟩ | ⟨hm, hx⟩) <;> rw [hm] <;>
  -- which we show by comparing the terms in the sum one by one
  gcongr with i hi
  · rcases eq_or_ne m 0 with rfl | hm
    · simp only [pow_zero, le_refl,
        show i = 0 by simpa only [zero_add, Finset.range_one, Finset.mem_singleton] using hi]
    · rw [pow_le_one_iff_of_nonneg (norm_nonneg _) hm] at hx
      exact pow_le_one₀ (norm_nonneg _) hx
  · contrapose! hx
    exact pow_le_one₀ (norm_nonneg _) hx.le
  · simpa [Nat.lt_succ_iff] using hi

Goal state after:
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : AddLeftMono α
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v
⊢ limsup u f + liminf v f ≤ limsup (u + v) f

Tactic:
have h := isCoboundedUnder_le_add h₄ h₂

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : AddLeftMono α
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (v + u)
⊢ limsup u f + liminf v f ≤ limsup (u + v) f
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : AddLeftMono α
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v
⊢ limsup u f + liminf v f ≤ limsup (u + v) f

Tactic:
by
  have h := isCoboundedUnder_le_add h₄ h₂ -- These `have` tactic improve performance.
  have h' := isBoundedUnder_le_add h₃ h₁
  rw [add_comm] at h h'
  refine add_le_of_forall_lt fun a a_u b b_v ↦ (le_limsup_iff h h').2 fun c c_ab ↦ ?_
  refine ((frequently_lt_of_lt_limsup h₂ a_u).and_eventually
    (eventually_lt_of_lt_liminf b_v h₄)).mono fun _ ab_x ↦ ?_
  exact c_ab.trans (add_lt_add ab_x.1 ab_x.2)

Goal state after: