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

Goal state before:
pp: case pos
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup U
inst✝⁴ : InnerProductSpace 𝕜 U
inst✝³ : FiniteDimensional 𝕜 U
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : CompleteSpace V
f : U →L[𝕜] V
this✝ : CompleteSpace U
this : CompleteSpace ↥(↑f).range
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
h : (↑f).ker = ⊥
⊢ ↑((↑f).normDet ^ 2) = (ContinuousLinearMap.adjoint f ∘SL f).det

pp: case neg
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup U
inst✝⁴ : InnerProductSpace 𝕜 U
inst✝³ : FiniteDimensional 𝕜 U
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : CompleteSpace V
f : U →L[𝕜] V
this✝ : CompleteSpace U
this : CompleteSpace ↥(↑f).range
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
h : ¬(↑f).ker = ⊥
⊢ ↑((↑f).normDet ^ 2) = (ContinuousLinearMap.adjoint f ∘SL f).det

Tactic:
· obtain ⟨b⟩ := (f.normDet_ne_zero_tfae.out 1 3).mp h
    have hf : f = f.range.subtypeₗᵢ.toContinuousLinearMap ∘L f.rangeRestrict := rfl
    conv_rhs => rw [hf]
    rw [ContinuousLinearMap.adjoint_comp, ← ContinuousLinearMap.comp_assoc,
      ContinuousLinearMap.comp_assoc (ContinuousLinearMap.adjoint _),
      f.range.subtypeₗᵢ.adjoint_comp_self, ContinuousLinearMap.one_def, ContinuousLinearMap.comp_id,
      ContinuousLinearMap.det, ContinuousLinearMap.toLinearMap_comp, ← det_toMatrix bu.toBasis,
      toMatrix_comp bu.toBasis b.toBasis bu.toBasis, ← ContinuousLinearMap.adjoint_toLinearMap,
      toMatrix_adjoint, f.toLinearMap.normDet_eq_norm_det_toMatrix_rangeRestrict bu b]
    simp [RCLike.conj_mul]

Goal state after:
case neg
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup U
inst✝⁴ : InnerProductSpace 𝕜 U
inst✝³ : FiniteDimensional 𝕜 U
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : CompleteSpace V
f : U →L[𝕜] V
this✝ : CompleteSpace U
this : CompleteSpace ↥(↑f).range
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
h : ¬(↑f).ker = ⊥
⊢ ↑((↑f).normDet ^ 2) = (ContinuousLinearMap.adjoint f ∘SL f).det
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
hrank : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction = 1
hrank' : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ = finrank ℝ V - 1
f : ℝ ≃L[ℝ] ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction :=
  (ContinuousLinearEquiv.toSpanNonzeroSingleton ℝ v hv).trans
    (ContinuousLinearEquiv.ofEq (ℝ ∙ v) (AffineSubspace.mk' p (ℝ ∙ v)).direction ⋯)
hf : MeasurableEmbedding ⇑f
p' : ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⟨p, ⋯⟩
g : ℝ → ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⇑(IsometryEquiv.vaddConst p') ∘ ⇑f
hadd : MeasurableEmbedding ⇑(IsometryEquiv.vaddConst p')
hg : MeasurableEmbedding g
hm : μHE[finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction] = ‖v‖ₑ • map g volume
⊢ μHE[finrank ℝ V] t = ‖v‖ₑ * ∫⁻ (x : ℝ), μHE[finrank ℝ V - 1] (t ∩ ↑(AffineSubspace.mk' (x • v +ᵥ p) (ℝ ∙ v)ᗮ))

Tactic:
have hx (x : ℝ) : x • v +ᵥ p = g x := by rfl

Goal state after:
V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
hrank : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction = 1
hrank' : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ = finrank ℝ V - 1
f : ℝ ≃L[ℝ] ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction :=
  (ContinuousLinearEquiv.toSpanNonzeroSingleton ℝ v hv).trans
    (ContinuousLinearEquiv.ofEq (ℝ ∙ v) (AffineSubspace.mk' p (ℝ ∙ v)).direction ⋯)
hf : MeasurableEmbedding ⇑f
p' : ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⟨p, ⋯⟩
g : ℝ → ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⇑(IsometryEquiv.vaddConst p') ∘ ⇑f
hadd : MeasurableEmbedding ⇑(IsometryEquiv.vaddConst p')
hg : MeasurableEmbedding g
hm : μHE[finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction] = ‖v‖ₑ • map g volume
hx : ∀ (x : ℝ), x • v +ᵥ p = ↑(g x)
⊢ μHE[finrank ℝ V] t = ‖v‖ₑ * ∫⁻ (x : ℝ), μHE[finrank ℝ V - 1] (t ∩ ↑(AffineSubspace.mk' (x • v +ᵥ p) (ℝ ∙ v)ᗮ))
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
this :
  1 ≤
    ⨅ t, ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ 0
⊢ ⨅ t, ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ 0 ≤
    ⨆ r,
      ⨆ (_ : 0 < r),
        ⨅ t,
          ⨅ (_ : {x} ⊆ ⋃ n, t n),
            ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ 0

Tactic:
convert! le_iSup₂ (α := ℝ≥0∞) (1 : ℝ≥0∞) zero_lt_one

Goal state after:
case e'_3
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
this :
  1 ≤
    ⨅ t, ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ 0
⊢ ⨅ t, ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ 0 =
    ⨅ t, ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ 0
Module: Mathlib.Analysis.InnerProductSpace.Trace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
x y : E
⊢ (trace 𝕜 E) ↑(((rankOne 𝕜) x) y) = ⟪y, x⟫_𝕜

Tactic:
rankOne_def',

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
x y : E
⊢ (trace 𝕜 E) ↑(ContinuousLinearMap.toSpanSingleton 𝕜 x ∘SL (innerSL 𝕜) y) = ⟪y, x⟫_𝕜
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
⊢ μH[↑(Fintype.card ι)] (univ.pi fun i ↦ Ioo ↑(a i) ↑(b i)) = ∏ x, volume ((fun i ↦ Ioo ↑(a i) ↑(b i)) x)

Tactic:
apply le_antisymm _

Goal state after:
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
⊢ ∏ x, volume ((fun i ↦ Ioo ↑(a i) ↑(b i)) x) ≤ μH[↑(Fintype.card ι)] (univ.pi fun i ↦ Ioo ↑(a i) ↑(b i))

ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
⊢ μH[↑(Fintype.card ι)] (univ.pi fun i ↦ Ioo ↑(a i) ↑(b i)) ≤ ∏ x, volume ((fun i ↦ Ioo ↑(a i) ↑(b i)) x)
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (o.areaForm (o.rightAngleRotation x)) y = -⟪x, y⟫

Tactic:
by
  rw [← o.inner_comp_rightAngleRotation, o.inner_rightAngleRotation_right, neg_neg]

Goal state after:
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
hs : Convex ℝ s
x : E
hx : (toWeakSpace 𝕜 E).toEquiv x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
this : ContinuousSMul ℝ E
⊢ (toWeakSpace 𝕜 E).toEquiv x ∈ (closure (⇑(toWeakSpace 𝕜 E) '' s))ᶜ

Tactic:
obtain ⟨f, u, hus, hux⟩ := RCLike.geometric_hahn_banach_closed_point (𝕜 := 𝕜)
    hs.closure isClosed_closure (by simpa using hx)

Goal state after:
𝕜 : 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
hs : Convex ℝ s
x : E
hx : (toWeakSpace 𝕜 E).toEquiv x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
this : ContinuousSMul ℝ E
f : StrongDual 𝕜 E
u : ℝ
hus : ∀ a ∈ closure s, RCLike.re (f a) < u
hux : u < RCLike.re (f x)
⊢ (toWeakSpace 𝕜 E).toEquiv x ∈ (closure (⇑(toWeakSpace 𝕜 E) '' s))ᶜ
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case neg.mp
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ((o.basisRightAngleRotation x hx).repr y) 0
⊢ 0 ≤ ⟪x, y⟫ ∧ (o.areaForm x) y = 0 → SameRay ℝ x y

Tactic:
let b : ℝ := (o.basisRightAngleRotation x hx).repr y 1

Goal state after:
case neg.mp
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ((o.basisRightAngleRotation x hx).repr y) 0
b : ℝ := ((o.basisRightAngleRotation x hx).repr y) 1
⊢ 0 ≤ ⟪x, y⟫ ∧ (o.areaForm x) y = 0 → SameRay ℝ x y
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
⊢ ((o.kahler x) a * (o.kahler a) y).re = (↑(‖a‖ ^ 2) * (o.kahler x) y).re

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
⊢ ((o.kahler x) a * (o.kahler a) y).im = (↑(‖a‖ ^ 2) * (o.kahler x) y).im

Tactic:
· simp only [o.kahler_apply_apply, Complex.add_im, Complex.add_re, Complex.I_im, Complex.I_re,
        Complex.mul_im, Complex.mul_re, Complex.ofReal_im, Complex.ofReal_re, Complex.real_smul]
      rw [real_inner_comm a x, o.areaForm_swap x a]
      linear_combination o.inner_mul_inner_add_areaForm_mul_areaForm a x y

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
⊢ ((o.kahler x) a * (o.kahler a) y).im = (↑(‖a‖ ^ 2) * (o.kahler x) y).im
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  IntegrableOn (fun x ↦ ↑(a * x) ^ (s - 1) • f (a * x)) (Ioi 0) volume ↔
    IntegrableOn (fun t ↦ ↑t ^ (s - 1) • f t) (Ioi 0) volume
h1 : EqOn (fun t ↦ ↑(a * t) ^ (s - 1) • f (a * t)) (↑a ^ (s - 1) • fun t ↦ ↑t ^ (s - 1) • f (a * t)) (Ioi 0)
h2 : ↑a ^ (s - 1) ≠ 0
⊢ MellinConvergent (fun t ↦ f (a * t)) s ↔ MellinConvergent f s

Tactic:
MellinConvergent,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  IntegrableOn (fun x ↦ ↑(a * x) ^ (s - 1) • f (a * x)) (Ioi 0) volume ↔
    IntegrableOn (fun t ↦ ↑t ^ (s - 1) • f t) (Ioi 0) volume
h1 : EqOn (fun t ↦ ↑(a * t) ^ (s - 1) • f (a * t)) (↑a ^ (s - 1) • fun t ↦ ↑t ^ (s - 1) • f (a * t)) (Ioi 0)
h2 : ↑a ^ (s - 1) ≠ 0
⊢ IntegrableOn (fun t ↦ ↑t ^ (s - 1) • f (a * t)) (Ioi 0) volume ↔ MellinConvergent f s
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  IntegrableOn (fun x ↦ ↑(a * x) ^ (s - 1) • f (a * x)) (Ioi 0) volume ↔
    IntegrableOn (fun t ↦ ↑t ^ (s - 1) • f t) (Ioi 0) volume
h1 : EqOn (fun t ↦ ↑(a * t) ^ (s - 1) • f (a * t)) (↑a ^ (s - 1) • fun t ↦ ↑t ^ (s - 1) • f (a * t)) (Ioi 0)
h2 : ↑a ^ (s - 1) ≠ 0
⊢ IntegrableOn (fun t ↦ ↑t ^ (s - 1) • f (a * t)) (Ioi 0) volume ↔ MellinConvergent f s

Tactic:
MellinConvergent,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  IntegrableOn (fun x ↦ ↑(a * x) ^ (s - 1) • f (a * x)) (Ioi 0) volume ↔
    IntegrableOn (fun t ↦ ↑t ^ (s - 1) • f t) (Ioi 0) volume
h1 : EqOn (fun t ↦ ↑(a * t) ^ (s - 1) • f (a * t)) (↑a ^ (s - 1) • fun t ↦ ↑t ^ (s - 1) • f (a * t)) (Ioi 0)
h2 : ↑a ^ (s - 1) ≠ 0
⊢ IntegrableOn (fun t ↦ ↑t ^ (s - 1) • f (a * t)) (Ioi 0) volume ↔
    IntegrableOn (fun t ↦ ↑t ^ (s - 1) • f t) (Ioi 0) volume
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
hf : MellinConvergent f ↑σ
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
⊢ Integrable g volume

Tactic:
MellinConvergent,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hf : IntegrableOn (fun t ↦ ↑t ^ (↑σ - 1) • f t) (Ioi 0) volume
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
⊢ Integrable g volume
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case c0
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ 0 ≤ (1 - ‖z‖)⁻¹

Tactic:
inv_nonneg

Goal state after:
case c0
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ 0 ≤ 1 - ‖z‖
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: a b : ℝ
f : ℝ → ℝ
s : ℝ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x ↦ x ^ (-a)
hs_top : s < a
hf_bot : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
hs_bot : b < s
c1 : ℝ
hc1 : 0 < c1
hc1' : IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioi c1) volume
c2 : ℝ
hc2 : 0 < c2
hc2' : IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioc 0 c2) volume
this : Ioi 0 = Ioc 0 c2 ∪ Ioc c2 c1 ∪ Ioi c1
⊢ ContinuousOn (fun t ↦ t ^ (s - 1)) (Ioi 0)

Tactic:
exact continuousOn_of_forall_continuousAt
    fun t ht ↦ continuousAt_rpow_const _ _ <| Or.inl <| ne_of_gt ht

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: 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
⊢ MellinConvergent f s

Tactic:
MellinConvergent,

Goal state after:
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
⊢ IntegrableOn (fun t ↦ ↑t ^ (s - 1) • f t) (Ioi 0) volume
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-a)
this : log =o[𝓝[>] 0] fun t ↦ t ^ (a - b)
t : ℝ
ht : t ∈ Ioi 0
⊢ (fun x ↦ x ^ (a - b) • x ^ (-a)) t = (fun x ↦ x ^ (-b)) t

Tactic:
simp_rw [smul_eq_mul, ← rpow_add ht]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-a)
this : log =o[𝓝[>] 0] fun t ↦ t ^ (a - b)
t : ℝ
ht : t ∈ Ioi 0
⊢ t ^ (a - b + -a) = t ^ (-b)
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: 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, 0 < v ∧ v < s.re - b ∧ v < a - s.re

Tactic:
by
    obtain ⟨w, hw1, hw2⟩ := exists_between (sub_pos.mpr hs_top)
    obtain ⟨w', hw1', hw2'⟩ := exists_between (sub_pos.mpr hs_bot)
    exact
      ⟨min w w', lt_min hw1 hw1', (min_le_right _ _).trans_lt hw2', (min_le_left _ _).trans_lt hw2⟩

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

Goal state before:
pp: ⊢ ConvexOn ℝ (Ioi 0) (log ∘ Γ)

Tactic:
refine convexOn_iff_forall_pos.mpr ⟨convex_Ioi _, fun x hx y hy a b ha hb hab => ?_⟩

Goal state after:
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
hy : y ∈ Ioi 0
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (log ∘ Γ) (a • x + b • y) ≤ a • (log ∘ Γ) x + b • (log ∘ Γ) y
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case hy
x : ℝ
n : ℕ
⊢ n ! ≠ 0

Tactic:
exact Nat.factorial_ne_zero n

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

Goal state before:
pp: 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))
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Tactic:
by
    refine this ⌈x - 1⌉₊ ?_ ?_
    · rcases lt_or_ge x 1 with ⟨⟩
      · rwa [Nat.ceil_eq_zero.mpr (by linarith : x - 1 ≤ 0), Nat.cast_zero]
      · convert! Nat.ceil_lt_add_one (by linarith : 0 ≤ x - 1)
        abel
    · rw [← sub_le_iff_le_add]; exact Nat.le_ceil _

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
aux3 : MeasurableSet (Ioc 0 1)
⊢ MellinConvergent ((Ioc 0 1).indicator fun x ↦ 1) s ∧
    ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • (Ioc 0 1).indicator (fun x ↦ 1) t = 1 / s

Tactic:
MellinConvergent,

Goal state after:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
aux3 : MeasurableSet (Ioc 0 1)
⊢ IntegrableOn (fun t ↦ ↑t ^ (s - 1) • (Ioc 0 1).indicator (fun x ↦ 1) t) (Ioi 0) volume ∧
    ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • (Ioc 0 1).indicator (fun x ↦ 1) t = 1 / s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case e'_5
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : ↑m < x - 1
hy' : x - 1 ≤ ↑m + 1
this✝ :
  ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n = logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)
hm : Tendsto (fun n ↦ logGammaSeq x n + x * (log (↑n + 1) - log ↑n)) atTop (𝓝 (f (x - 1) - f 1 + log (x - 1)))
this :
  ((fun x_1 ↦
        (fun n ↦ logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)) x_1 +
          (fun b ↦ log (x - 1)) x_1) ∘
      fun a ↦ a + 1) =
    fun n ↦ logGammaSeq x n + x * (log (↑n + 1) - log ↑n)
⊢ f x - f 1 = f (x - 1) - f 1 + log (x - 1) - x * 0

Tactic:
have := hf_feq ((Nat.cast_nonneg m).trans_lt hy)
      rw [sub_add_cancel] at this
      rw [this]
      ring

Goal state after:
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
F : ι → 𝕜 → 𝕜'
d : ι → ℤ
hd : (support d).Finite
h : ∀ (i : ι), MeromorphicOn (F i) U
h' : ∀ (i : ι), ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
hA : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ hd.toFinset, AnalyticAt 𝕜 (F i) y
⊢ logDeriv (∏ᶠ (i : ι), F i ^ d i) =ᶠ[codiscreteWithin U] fun z ↦ ∑ᶠ (i : ι), d i • logDeriv (F i) z

Tactic:
have hN : ∀ᶠ y in codiscreteWithin U, ∀ i ∈ hd.toFinset, F i y ≠ 0 :=
    (eventually_all_finset hd.toFinset).2 fun i _ ↦ (h i).eventually_codiscreteWithin_apply_ne_zero
      (h' i)

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
F : ι → 𝕜 → 𝕜'
d : ι → ℤ
hd : (support d).Finite
h : ∀ (i : ι), MeromorphicOn (F i) U
h' : ∀ (i : ι), ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
hA : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ hd.toFinset, AnalyticAt 𝕜 (F i) y
hN : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ hd.toFinset, F i y ≠ 0
⊢ logDeriv (∏ᶠ (i : ι), F i ^ d i) =ᶠ[codiscreteWithin U] fun z ↦ ∑ᶠ (i : ι), d i • logDeriv (F i) z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_5
x : ℝ
⊢ 𝓝 (sin (π * x)) = 𝓝 (Complex.sin ↑(π * x)).re

Tactic:
← Complex.ofReal_sin,

Goal state after:
case e'_5
x : ℝ
⊢ 𝓝 (sin (π * x)) = 𝓝 (↑(sin (π * x))).re
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
v : V
c : k
hc : 0 < c
p : P
⊢ atTop • 𝓝 (c • v) +ᵥ pure p = atTop • 𝓝 v +ᵥ pure p

Tactic:
← show map (c • ·) (𝓝 v) = 𝓝 (c • v) from
      (Homeomorph.smulOfNeZero c hc.ne').map_nhds_eq v,

Goal state after:
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
v : V
c : k
hc : 0 < c
p : P
⊢ atTop • map (fun x ↦ c • x) (𝓝 v) +ᵥ pure p = atTop • 𝓝 v +ᵥ pure p
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
v : V
p : P → Prop
c : k
u : V
⊢ 0 < (c, u).1 →
    ((∀ᶠ (y : P) in asymptoticNhds k P ((c, u).1 • (c, u).2), p y) ↔ ∀ᶠ (y : P) in asymptoticNhds k P (c, u).2, p y)

Tactic:
(hc : 0 < c)

Goal state after:
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
v : V
p : P → Prop
c : k
u : V
hc : 0 < c
⊢ (∀ᶠ (y : P) in asymptoticNhds k P ((c, u).1 • (c, u).2), p y) ↔ ∀ᶠ (y : P) in asymptoticNhds k P (c, u).2, p y
Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : SeminormedAddCommGroup V
inst✝⁵ : SeminormedAddCommGroup W
inst✝⁴ : SeminormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖f‖ * ‖g‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖

Tactic:
le_add_iff_nonneg_right

Goal state after:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : SeminormedAddCommGroup V
inst✝⁵ : SeminormedAddCommGroup W
inst✝⁴ : SeminormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ 0 ≤ ‖f 0‖