mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ⇑(toWeakSpace 𝕜 E) '' closure s = closure (⇑(toWeakSpace 𝕜 E) '' s)

Tactic:
refine le_antisymm (map_continuous <| toWeakSpaceCLM 𝕜 E).continuousOn.image_closure
    (Set.compl_subset_compl.mp fun x 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 : WeakSpace 𝕜 E
hx : x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
⊢ x ∈ (closure (⇑(toWeakSpace 𝕜 E) '' s))ᶜ
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
hx : ¬x = 0
a : ℝ := ((o.basisRightAngleRotation x hx).repr y) 0
b : ℝ := ((o.basisRightAngleRotation x hx).repr y) 1
this : 0 ≤ a * ‖x‖ ^ 2 ∧ b * ‖x‖ ^ 2 = 0 → SameRay ℝ x (a • x + b • o.rightAngleRotation x)
⊢ 0 ≤ ⟪x, y⟫ ∧ (o.areaForm x) y = 0 → SameRay ℝ x y

Tactic:
by
      rw [← (o.basisRightAngleRotation x hx).sum_repr y]
      simp only [Fin.sum_univ_succ, coe_basisRightAngleRotation, Matrix.cons_val_zero,
        Fin.succ_zero_eq_one', Finset.univ_eq_empty, Finset.sum_empty, areaForm_apply_self,
        map_smul, map_add, real_inner_smul_right, inner_add_right, Matrix.cons_val_one,
        smul_eq_mul, areaForm_rightAngleRotation_right,
        mul_zero, add_zero, zero_add, neg_zero, inner_rightAngleRotation_right,
        real_inner_self_eq_norm_sq]
      exact this

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

Goal state before:
pp: z : ℂ
⊢ Complex.orientation.rightAngleRotation z = I * z

Tactic:
apply ext_inner_right ℝ
  intro w
  rw [Orientation.inner_rightAngleRotation_left]
  simp only [Complex.areaForm, Complex.inner, mul_re, mul_im, conj_re, conj_im, map_mul, conj_I,
    neg_re, neg_im, I_re, I_im]
  ring

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case refine_1
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ (b : ℝ), e ≤ b → ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
⊢ AEStronglyMeasurable (fun t ↦ t ^ (s - 1) * f t) (volume.restrict (Ioi (max e 1)))

Tactic:
refine AEStronglyMeasurable.mul ?_ (hfc.mono_set (Ioi_subset_Ioi he'.le))

Goal state after:
case refine_1
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ (b : ℝ), e ≤ b → ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
⊢ AEStronglyMeasurable (fun t ↦ t ^ (s - 1)) (volume.restrict (Ioi (max e 1)))
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ (b : ℝ), e ≤ b → ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
t : ℝ
ht : t ∈ Ioi (max e 1)
ht' : 0 < t
⊢ ‖t ^ (s - 1)‖ * ‖f t‖ ≤ t ^ (s - 1) * (‖t ^ (-a)‖ * d)

Tactic:
mul_comm _ d,

Goal state after:
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ (b : ℝ), e ≤ b → ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
t : ℝ
ht : t ∈ Ioi (max e 1)
ht' : 0 < t
⊢ ‖t ^ (s - 1)‖ * ‖f t‖ ≤ t ^ (s - 1) * (d * ‖t ^ (-a)‖)
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ (b : ℝ), e ≤ b → ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
t : ℝ
ht : t ∈ Ioi (max e 1)
ht' : 0 < t
⊢ t ^ (s - 1) * ‖f t‖ ≤ t ^ (s - 1) * (d * ‖t ^ (-a)‖)

Tactic:
gcongr

Goal state after:
case hbc
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ (b : ℝ), e ≤ b → ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
t : ℝ
ht : t ∈ Ioi (max e 1)
ht' : 0 < t
⊢ ‖f t‖ ≤ d * ‖t ^ (-a)‖
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
ε : ℝ
hε : 0 < ε
t : ℝ
hε' : ‖f t‖ ≤ d * ‖t ^ (-b)‖
ht : t ∈ Ioo 0 ε
⊢ ‖f t‖ * ‖t ^ (s - 1)‖ ≤ d * ‖t ^ (-b)‖ * ‖t ^ (s - 1)‖

Tactic:
gcongr

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z ↦ log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z ↦ (-z) ^ n * (1 + z)⁻¹
hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
hcont : ContinuousOn (fun t ↦ f' (0 + ↑t * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-(↑t * z)) ^ n * (1 + ↑t * z)⁻¹
t : ℝ
ht₀ : 0 < t
ht₁ : t ≤ 1
⊢ t ^ n * ‖(1 + ↑t * z)⁻¹‖ ≤ t ^ n * (1 - ‖z‖)⁻¹

Tactic:
gcongr

Goal state after:
case hbc
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := ⋯
f' : ℂ → ℂ := ⋯
hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
hcont : ContinuousOn (fun t ↦ f' (0 + ↑t * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-(↑t * z)) ^ n * (1 + ↑t * z)⁻¹
t : ℝ
ht₀ : 0 < t
ht₁ : t ≤ 1
⊢ ‖(1 + ↑t * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
this : (1 - ‖z‖)⁻¹ ≤ 2
⊢ (1 - ‖z‖)⁻¹ / (↑n + 1) * ‖z‖ ^ (n + 1) ≤ 2 / (↑n + 1) * ‖z‖ ^ (n + 1)

Tactic:
gcongr

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

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

Tactic:
gcongr

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

case h₁
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ ‖z‖ ^ 2 ≤ ‖z‖ / 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

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

Tactic:
gcongr

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case refine_1.inr
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ ‖z‖ ^ n / ↑n ≤ ‖z‖ ^ n / 1

Tactic:
gcongr

Goal state after:
case hdb
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ 1 ≤ ↑n
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case refine_2
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)
t : ℝ
ht : t ∈ Ioi 0
⊢ ((fun x ↦ x ^ (b - a)) ∘ fun x ↦ x⁻¹) t = (fun t ↦ t ^ (a - b)) t

Tactic:
simp_rw [Function.comp_apply, inv_rpow (le_of_lt ht), ← rpow_neg (le_of_lt ht), neg_sub]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case succ
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ (1 - ‖z‖)⁻¹ * ‖z‖ ^ (n + 1) / (↑n + 1) ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖z‖ ^ (n + 1) / 1

Tactic:
gcongr

Goal state after:
case hbc
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ (1 - ‖z‖)⁻¹ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹

case hdb
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ 1 ≤ ↑n + 1
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)
f_mem_Lp : ∀ {c u : ℝ}, 0 < c → 0 < u → MemLp (f c u) (ENNReal.ofReal (1 / c)) (volume.restrict (Ioi 0))
x : ℝ
hx : x ∈ Ioi 0
A : rexp (-x) = rexp (-a * x) * rexp (-b * x)
⊢ x ^ (a * s + b * t - 1) = x ^ (a * (s - 1)) * x ^ (b * (t - 1))

Tactic:
rw [← rpow_add hx, hab']

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)
f_mem_Lp : ∀ {c u : ℝ}, 0 < c → 0 < u → MemLp (f c u) (ENNReal.ofReal (1 / c)) (volume.restrict (Ioi 0))
x : ℝ
hx : x ∈ Ioi 0
A : rexp (-x) = rexp (-a * x) * rexp (-b * x)
⊢ x ^ (a * s + (1 - a) * t - 1) = x ^ (a * (s - 1) + (1 - a) * (t - 1))
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 : ℝ
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 : z ∈ Metric.ball s v
⊢ ‖↑t ^ (z - 1)‖ * (|log t| * ‖f t‖) ≤ (t ^ (s.re + v - 1) + t ^ (s.re - v - 1)) * (|log t| * ‖f t‖)

Tactic:
gcongr

Goal state after:
case hbc
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 := ⋯
F' : ℂ → ℝ → E := ⋯
v : ℝ
hv0 : 0 < v
hv1 : v < s.re - b
hv2 : v < a - s.re
bound : ℝ → ℝ := ⋯
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 : z ∈ Metric.ball s v
⊢ ‖↑t ^ (z - 1)‖ ≤ t ^ (s.re + v - 1) + t ^ (s.re - v - 1)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ log (Γ (a * x + (1 - a) * y)) ≤ log (Γ x ^ a * Γ y ^ (1 - a))

Tactic:
gcongr

Goal state after:
case hxy
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ Γ (a * x + (1 - a) * y) ≤ Γ x ^ a * Γ y ^ (1 - a)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_2
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ z ^ 2 / (↑n + 1) ^ 2 = 4 * z ^ 2 / (2 * ↑n + 2 * 1) ^ 2

Tactic:
← mul_add,

Goal state after:
case e'_2
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ z ^ 2 / (↑n + 1) ^ 2 = 4 * z ^ 2 / (2 * (↑n + 1)) ^ 2
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 : 2 ≤ n
hx : 0 < x
⊢ 0 < ↑n - ↑1

Tactic:
sub_pos,

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 : 2 ≤ n
hx : 0 < x
⊢ ↑1 < ↑n
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)

Goal state after:
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)
this : f (x - 1 + 1) = f (x - 1) + log (x - 1)
⊢ f x - f 1 = f (x - 1) - f 1 + log (x - 1) - x * 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case succ
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
hm : ∀ {x : ℝ}, 0 < x → ↑m < x → x ≤ ↑m + 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
x : ℝ
hx : 0 < x
⊢ ↑(m + 1) < x → x ≤ ↑(m + 1) + 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Tactic:
| succ m hm =>

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

Goal state before:
pp: x : ℝ
hx : 0 < x
this : log (Γ x) = (log ∘ Γ) x - (log ∘ Γ) 1
⊢ Tendsto (logGammaSeq x) atTop (𝓝 ((log ∘ Γ) x - (log ∘ Γ) 1))

Tactic:
refine BohrMollerup.tendsto_logGammaSeq convexOn_log_Gamma (fun {y} hy => ?_) hx

Goal state after:
x : ℝ
hx : 0 < x
this : log (Γ x) = (log ∘ Γ) x - (log ∘ Γ) 1
y : ℝ
hy : 0 < y
⊢ (log ∘ Γ) (y + 1) = (log ∘ Γ) y + log y
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: ⊢ Γ (3 / 2) < 1

Tactic:
have A : (0 : ℝ) < 3 / 2 := by simp
  have :=
    BohrMollerup.f_add_nat_le convexOn_log_Gamma (fun {y} hy => ?_) two_ne_zero one_half_pos
      (by norm_num : 1 / 2 ≤ (1 : ℝ))
  swap
  · rw [Function.comp_apply, Gamma_add_one hy.ne', log_mul hy.ne' (Gamma_pos_of_pos hy).ne',
      add_comm, Function.comp_apply]
  rw [Function.comp_apply, Function.comp_apply, Nat.cast_two, Gamma_two, log_one, zero_add,
    (by norm_num : (2 : ℝ) + 1 / 2 = 3 / 2 + 1), Gamma_add_one A.ne',
    log_mul A.ne' (Gamma_pos_of_pos A).ne', ← le_sub_iff_add_le',
    log_le_iff_le_exp (Gamma_pos_of_pos A)] at this
  refine this.trans_lt (exp_lt_one_iff.mpr ?_)
  rw [mul_comm, ← mul_div_assoc, div_sub' two_ne_zero]
  refine div_neg_of_neg_of_pos ?_ two_pos
  rw [sub_neg, mul_one, ← Nat.cast_two, ← log_pow, ← exp_lt_exp, Nat.cast_two, exp_log two_pos,
      exp_log] <;>
    norm_num

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

Goal state before:
pp: case succ.refine_1
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
⊢ 0 < (↑n.succ).re

pp: case succ.refine_2
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : u * u.betaIntegral (↑n.succ + 1) = ↑n.succ * (u + 1).betaIntegral ↑n.succ
⊢ u.betaIntegral (↑(n + 1) + 1) = ↑(n + 1)! / ∏ j ∈ Finset.range (n + 1 + 1), (u + ↑j)

Tactic:
· rw [← ofReal_natCast, ofReal_re]; positivity

Goal state after:
case succ.refine_2
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : u * u.betaIntegral (↑n.succ + 1) = ↑n.succ * (u + 1).betaIntegral ↑n.succ
⊢ u.betaIntegral (↑(n + 1) + 1) = ↑(n + 1)! / ∏ j ∈ Finset.range (n + 1 + 1), (u + ↑j)
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : ↑s → Finset ι
hfs : ∀ (i : ↑s), ↑i ∈ fs i
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]
⊢ ∃ w' fs',
    ∑ j ∈ fs', w' j = 1 ∧
      (Finset.affineCombination k fs' p) w' = p' ∧
        ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * (↑(fs i) \ {↑i}).indicator (w i) j = (↑fs' \ {↑i}).indicator w' j

Tactic:
have hp'' : ∀ i : s, ∃ r : k, (fs i).affineCombination k p
      (AffineMap.lineMap (Pi.single (i : ι) 1) (w i) r) = p' := by
    intro i
    simp_rw [mem_affineSpan_pair_iff_exists_lineMap_eq] at hp'
    obtain ⟨r, rfl⟩ := hp' i
    exact ⟨r, by simp [hfs]⟩

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : ↑s → Finset ι
hfs : ∀ (i : ↑s), ↑i ∈ fs i
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]
hp'' : ∀ (i : ↑s), ∃ r, (Finset.affineCombination k (fs i) p) ((AffineMap.lineMap (Pi.single (↑i) 1) (w i)) r) = p'
⊢ ∃ w' fs',
    ∑ j ∈ fs', w' j = 1 ∧
      (Finset.affineCombination k fs' p) w' = p' ∧
        ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * (↑(fs i) \ {↑i}).indicator (w i) j = (↑fs' \ {↑i}).indicator w' j
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case inr
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : x ≤ ↑n
⊢ (1 - x / ↑n) ^ n * x ^ (s.re - 1) ≤ rexp (-x) * x ^ (s.re - 1)

Tactic:
gcongr

Goal state after:
case hbc
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := ⋯
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : x ≤ ↑n
⊢ (1 - x / ↑n) ^ n ≤ rexp (-x)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
this : ∀ (m : ℕ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))

Tactic:
by tauto

Goal state after:
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 0‖ + ‖f 0‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖

Tactic:
g.norm_image_zero_le

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
⊢ ‖f‖ * ‖g‖ + ‖f 0‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

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

Tactic:
ofReal_inj

Goal state after:
case pos
s : ℂ
h_im : s.im = 0
this : s = ↑s.re
n : ℕ
hs : s.re = -↑n
⊢ s.re = -↑n
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case neg
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
this : sin (↑π * s) ≠ 0
⊢ Gamma s ≠ 0

Tactic:
have A := div_ne_zero (ofReal_ne_zero.mpr Real.pi_pos.ne') this

Goal state after:
case neg
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
this : sin (↑π * s) ≠ 0
A : ↑π / sin (↑π * s) ≠ 0
⊢ Gamma s ≠ 0
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: 𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst✝¹¹ : SeminormedCommRing S
inst✝¹⁰ : SeminormedRing R
inst✝⁹ : SeminormedAddCommGroup M
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsBoundedSMul S R
inst✝⁵ : IsBoundedSMul S M
inst✝⁴ : Module R M
inst✝³ : IsBoundedSMul R M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : IsBoundedSMul Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ ‖r₁ * r₂‖ + ‖r₁ • m₂ + MulOpposite.op r₂ • m₁‖ ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖)

Tactic:
gcongr

Goal state after:
case h₁
𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst✝¹¹ : SeminormedCommRing S
inst✝¹⁰ : SeminormedRing R
inst✝⁹ : SeminormedAddCommGroup M
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsBoundedSMul S R
inst✝⁵ : IsBoundedSMul S M
inst✝⁴ : Module R M
inst✝³ : IsBoundedSMul R M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : IsBoundedSMul Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ ‖r₁ * r₂‖ ≤ ‖r₁‖ * ‖r₂‖

case h₂
𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst✝¹¹ : SeminormedCommRing S
inst✝¹⁰ : SeminormedRing R
inst✝⁹ : SeminormedAddCommGroup M
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsBoundedSMul S R
inst✝⁵ : IsBoundedSMul S M
inst✝⁴ : Module R M
inst✝³ : IsBoundedSMul R M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : IsBoundedSMul Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ ‖r₁ • m₂ + MulOpposite.op r₂ • m₁‖ ≤ ‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖
Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential

Goal state before:
pp: m : Type u_1
n' : m → Type u_3
𝔸 : Type u_5
inst✝⁸ : Fintype m
inst✝⁷ : DecidableEq m
inst✝⁶ : (i : m) → Fintype (n' i)
inst✝⁵ : (i : m) → DecidableEq (n' i)
inst✝⁴ : Ring 𝔸
inst✝³ : TopologicalSpace 𝔸
inst✝² : IsTopologicalRing 𝔸
inst✝¹ : T2Space 𝔸
inst✝ : Algebra ℚ 𝔸
v : (i : m) → Matrix (n' i) (n' i) 𝔸
⊢ ∑' (n : ℕ), (↑n.factorial)⁻¹ • blockDiagonal' v ^ n = blockDiagonal' (∑' (n : ℕ), (↑n.factorial)⁻¹ • v ^ n)

Tactic:
← blockDiagonal'_pow,

Goal state after:
m : Type u_1
n' : m → Type u_3
𝔸 : Type u_5
inst✝⁸ : Fintype m
inst✝⁷ : DecidableEq m
inst✝⁶ : (i : m) → Fintype (n' i)
inst✝⁵ : (i : m) → DecidableEq (n' i)
inst✝⁴ : Ring 𝔸
inst✝³ : TopologicalSpace 𝔸
inst✝² : IsTopologicalRing 𝔸
inst✝¹ : T2Space 𝔸
inst✝ : Algebra ℚ 𝔸
v : (i : m) → Matrix (n' i) (n' i) 𝔸
⊢ ∑' (n : ℕ), (↑n.factorial)⁻¹ • blockDiagonal' (v ^ n) = blockDiagonal' (∑' (n : ℕ), (↑n.factorial)⁻¹ • v ^ n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series

Goal state before:
pp: z : ℂ
this :
  HasSum ((fun i ↦ ((z * I) ^ i / ↑i ! + (-z * I) ^ i / ↑i !) / 2) ∘ ⇑(Nat.divModEquiv 2).symm)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
⊢ HasSum (fun n ↦ (z * I) ^ (2 * n) / ↑(2 * n)!) ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)

Tactic:
dsimp [Function.comp_def] at this

Goal state after:
z : ℂ
this :
  HasSum
    (fun x ↦ ((z * I) ^ (x.1 * 2 + ↑x.2) / ↑(x.1 * 2 + ↑x.2)! + (-z * I) ^ (x.1 * 2 + ↑x.2) / ↑(x.1 * 2 + ↑x.2)!) / 2)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
⊢ HasSum (fun n ↦ (z * I) ^ (2 * n) / ↑(2 * n)!) ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: ⊢ ‖1‖ = 1

Tactic:
by rw [norm_eq_sqrt_real_inner, inner_self, normSq.map_one, Real.sqrt_one]

Goal state after: