mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
⊢ ∑' (n : ℕ), ⨆ (_ : (id t n).Nonempty), ⨅ (_ : ediam (id t n) ≤ r), m (ediam (id t n)) =
    ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ id r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n))

Tactic:
dsimp

Goal state after:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
⊢ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)) =
    ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n))
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
hs : s.Subsingleton
d : ℝ
hd : 0 ≤ d
⊢ μH[d] s ≤ 1

Tactic:
rcases eq_empty_or_nonempty s with (rfl | ⟨x, hx⟩)

Goal state after:
case inl
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d : ℝ
hd : 0 ≤ d
hs : ∅.Subsingleton
⊢ μH[d] ∅ ≤ 1

case inr
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
hs : s.Subsingleton
d : ℝ
hd : 0 ≤ d
x : X
hx : x ∈ s
⊢ μH[d] s ≤ 1
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case inl
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
r : ℝ≥0
f : X → Y
s : Set X
hr : 0 < r
d : ℝ
hd : 0 ≤ d
h : HolderOnWith 0 r f s
⊢ μH[d] (f '' s) ≤ ↑0 ^ d * μH[↑r * d] s

Tactic:
rcases eq_empty_or_nonempty s with (rfl | ⟨x, hx⟩)

Goal state after:
case inl.inl
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
r : ℝ≥0
f : X → Y
hr : 0 < r
d : ℝ
hd : 0 ≤ d
h : HolderOnWith 0 r f ∅
⊢ μH[d] (f '' ∅) ≤ ↑0 ^ d * μH[↑r * d] ∅

case inl.inr
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
r : ℝ≥0
f : X → Y
s : Set X
hr : 0 < r
d : ℝ
hd : 0 ≤ d
h : HolderOnWith 0 r f s
x : X
hx : x ∈ s
⊢ μH[d] (f '' s) ≤ ↑0 ^ d * μH[↑r * d] s
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case inr.refine_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
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
d : ℝ
hd : 0 ≤ d
hC0 : 0 < C
hCd0 : ↑C ^ d ≠ 0
hCd : ↑C ^ d ≠ ∞
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (fun d ↦ ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → ↑C * x ^ ↑r < R
t : ℕ → Set X
hst : s ⊆ ⋃ n, t n
⊢ f '' s ⊆ ⋃ n, (fun n ↦ f '' (t n ∩ s)) n

Tactic:
grw [← image_iUnion, ← iUnion_inter, ← hst, inter_self]

Goal state after:
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:
dsimp

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 ≤ ↑(‖r‖₊ ^ d)⁻¹ * μH[d] (r • s)
Module: Mathlib.Analysis.LocallyConvex.PointwiseConvergence

Goal state before:
pp: α : Type u_1
R : Type u_2
𝕜₁ : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₃ →+* 𝕜₂
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜₁ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜₂ F
x : E
A B : E →SLₚₜ[σ] F
⊢ ‖(A + B) x‖ ≤ ‖A x‖ + ‖B x‖

Tactic:
by simpa only using! norm_add_le _ _

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)
f : F →L[𝕜] 𝕜
⊢ Continuous (e.dualMap ↑f).toFun

Tactic:
dsimp

Goal state after:
𝕜 : 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)
f : F →L[𝕜] 𝕜
⊢ Continuous ⇑(e.dualMap ↑f)
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
hE : CompleteSpace E
⊢ mellin (fun t ↦ f (t ^ 0)) s = |0|⁻¹ • mellin f (s / ↑0)

Tactic:
simp [integral_smul_const, mellin, setIntegral_Ioi_zero_cpow]

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)
⊢ ContinuousOn (fun t ↦ f' (0 + ↑t * z)) (Set.Icc 0 1)

Tactic:
simp only [zero_add]

Goal state after:
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)
⊢ ContinuousOn (fun t ↦ f' (↑t * z)) (Set.Icc 0 1)
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

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

Tactic:
by
  convert! norm_log_sub_logTaylor_le 1 hz using 2
  · simp [logTaylor_succ, logTaylor_zero, sub_eq_add_neg]
  · norm_num

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ x ∈ uIcc 0 (π / 2), HasDerivAt (fun y ↦ ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ ∫ (x : ℝ) in 0..π / 2, ↑n / (2 * z) * (Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1)) =
    ∫ (x : ℝ) in 0..π / 2, -(-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1) * (Complex.sin (2 * z * ↑x) / (2 * z)))

Tactic:
refine integral_congr fun x _ => ?_

Goal state after:
case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ x ∈ uIcc 0 (π / 2), HasDerivAt (fun y ↦ ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ ↑n / (2 * z) * (Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1)) =
    -(-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1) * (Complex.sin (2 * z * ↑x) / (2 * z)))
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
| ‖z‖ ^ n

Tactic:
rw [← div_one (‖z‖ ^ n)]

Goal state after:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
| ‖z‖ ^ n / 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_2
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ ∫ (x : ℝ) in 0..π / 2, Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1) =
    ∫ (x : ℝ) in 0..π / 2, ↑(sin x) * ↑(cos x) ^ (n - 1) * Complex.sin (2 * z * ↑x)

Tactic:
refine integral_congr fun x _ => ?_

Goal state after:
case e'_2
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1) = ↑(sin x) * ↑(cos x) ^ (n - 1) * Complex.sin (2 * z * ↑x)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ (↑n / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
      (↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2) =
    ↑(sin (π / 2)) * ↑(cos (π / 2)) ^ (n - 1) * (-Complex.cos (2 * z * ↑(π / 2)) / (2 * z)) -
        ↑(sin 0) * ↑(cos 0) ^ (n - 1) * (-Complex.cos (2 * z * ↑0) / (2 * z)) -
      ∫ (x : ℝ) in 0..π / 2,
        (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) * (-Complex.cos (2 * z * ↑x) / (2 * z))

Tactic:
rw [sin_zero, cos_pi_div_two, Complex.ofReal_zero, zero_pow, zero_mul,
      mul_zero, zero_mul, zero_mul, sub_zero, zero_sub, ←
      integral_neg, ← integral_const_mul, ← integral_const_mul, ← integral_sub]

Goal state after:
case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ ∫ (x : ℝ) in 0..π / 2,
      ↑n / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
        (↑n - 1) / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2)) =
    ∫ (x : ℝ) in 0..π / 2,
      -((↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) * (-Complex.cos (2 * z * ↑x) / (2 * z)))

case e'_3.hf
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ IntervalIntegrable (fun x ↦ ↑n / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n)) volume 0 (π / 2)

case e'_3.hg
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ IntervalIntegrable (fun x ↦ (↑n - 1) / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2))) volume 0 (π / 2)

case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ n - 1 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

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

Tactic:
dsimp

Goal state after:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun x ↦ ↑x * g x) atTop (𝓝 t)
hg0 : Tendsto g atTop (𝓝 0)
x : ℝ
hg1 : g x ≠ -1
⊢ cexp (↑x * log (1 + g x)) = (1 + g x) ^ ↑x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ ∫ (x : ℝ) in 0..π / 2,
      ↑n / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
        (↑n - 1) / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2)) =
    ∫ (x : ℝ) in 0..π / 2,
      -((↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) * (-Complex.cos (2 * z * ↑x) / (2 * z)))

Tactic:
refine integral_congr fun x _ => ?_

Goal state after:
case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ ↑n / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
      (↑n - 1) / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2)) =
    -((↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) * (-Complex.cos (2 * z * ↑x) / (2 * z)))
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case hbc.inl
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 - s‖ < v
h : 1 ≤ t
⊢ z.re ≤ s.re + v

Tactic:
have hz' := (re_le_norm _).trans hz.le

Goal state after:
case hbc.inl
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 - s‖ < v
h : 1 ≤ t
hz' : (z - s).re ≤ v
⊢ z.re ≤ s.re + v
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
⊢ s.re - v ≤ z.re

Tactic:
have hz' := (re_le_norm _).trans hz.le

Goal state after:
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
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e_a
n : ℕ
L : IntervalIntegrable (fun i ↦ sin i ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun i ↦ sin i ^ n) volume (π / 2) π
⊢ ∫ (x : ℝ) in 0..π / 2, cos (π / 2 - x) ^ n = ∫ (x : ℝ) in 0..π / 2, sin x ^ n

Tactic:
refine integral_congr fun x _ => ?_

Goal state after:
case e_a
n : ℕ
L : IntervalIntegrable (fun i ↦ sin i ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun i ↦ sin i ^ n) volume (π / 2) π
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ cos (π / 2 - x) ^ n = sin x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e_a
n : ℕ
L : IntervalIntegrable (fun i ↦ sin i ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun i ↦ sin i ^ n) volume (π / 2) π
⊢ ∫ (x : ℝ) in 0..π / 2, cos x ^ n = ∫ (x : ℝ) in 0..π / 2, sin (x + π / 2) ^ n

Tactic:
refine integral_congr fun x _ => ?_

Goal state after:
case e_a
n : ℕ
L : IntervalIntegrable (fun i ↦ sin i ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun i ↦ sin i ^ n) volume (π / 2) π
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ cos x ^ n = sin (x + π / 2) ^ n
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: s : ℂ
hs : 0 < s.re
⊢ HasMellin ((Ioc 0 1).indicator fun x ↦ 1) s (1 / s)

Tactic:
have aux1 : -1 < (s - 1).re := by
    simpa only [sub_re, one_re, sub_eq_add_neg] using! lt_add_of_pos_left _ hs
  have aux2 : s ≠ 0 := by contrapose! hs; rw [hs, zero_re]
  have aux3 : MeasurableSet (Ioc (0 : ℝ) 1) := measurableSet_Ioc
  simp_rw [HasMellin, mellin, MellinConvergent, ← indicator_smul, IntegrableOn,
    integrable_indicator_iff aux3, smul_eq_mul, integral_indicator aux3, mul_one, IntegrableOn,
    Measure.restrict_restrict_of_subset Ioc_subset_Ioi_self]
  rw [← IntegrableOn, ← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]
  refine ⟨intervalIntegral.intervalIntegrable_cpow' aux1, ?_⟩
  rw [← intervalIntegral.integral_of_le zero_le_one, integral_cpow (Or.inl aux1), sub_add_cancel,
    ofReal_zero, ofReal_one, one_cpow, zero_cpow aux2, sub_zero]

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

Goal state before:
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 [mul_comm u _, ← eq_div_iff] at this

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.betaIntegral (↑n.succ + 1) = ↑n.succ * (u + 1).betaIntegral ↑n.succ / u
⊢ u.betaIntegral (↑(n + 1) + 1) = ↑(n + 1)! / ∏ j ∈ Finset.range (n + 1 + 1), (u + ↑j)

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.betaIntegral (↑n.succ + 1) * u = ↑n.succ * (u + 1).betaIntegral ↑n.succ
⊢ u ≠ 0
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case refine_2
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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : s.Regular
σ : Equiv.Perm (Fin (n + 1))
x : P ≃ᵢ P
hx : s.points ∘ ⇑((e.trans σ).trans e.symm) = ⇑x ∘ s.points
i : Fin (n + 1)
⊢ ((s.reindex e).points ∘ ⇑σ) i = (⇑x ∘ (s.reindex e).points) i

Tactic:
simpa using congrFun hx (e.symm i)

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

Goal state before:
pp: 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
⊢ dist (s.points i) (s.points j) = dist (s.points 0) (s.points 1)

Tactic:
have hn : n ≠ 0 := by lia

Goal state after:
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
⊢ dist (s.points i) (s.points j) = dist (s.points 0) (s.points 1)
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: case inr
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormOneClass F
inst✝¹ : NormMulClass F
inst✝ : NormedAlgebra ℂ F
x : F
z : ℂ
hz : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℂ F) x_1‖) Set.univ z
M : ℝ := ‖x - (algebraMap ℂ F) z‖
hM : M = ‖x - (algebraMap ℂ F) z‖
hM₀ : 0 < M
H : ∀ (z : ℂ), ‖x - (algebraMap ℂ F) z‖ ≠ 0
key : |‖x‖ + M + 1| - ‖x‖ ≤ M
⊢ False

Tactic:
abs_of_nonneg (by positivity)

Goal state after:
case inr
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormOneClass F
inst✝¹ : NormMulClass F
inst✝ : NormedAlgebra ℂ F
x : F
z : ℂ
hz : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℂ F) x_1‖) Set.univ z
M : ℝ := ‖x - (algebraMap ℂ F) z‖
hM : M = ‖x - (algebraMap ℂ F) z‖
hM₀ : 0 < M
H : ∀ (z : ℂ), ‖x - (algebraMap ℂ F) z‖ ≠ 0
key : ‖x‖ + M + 1 - ‖x‖ ≤ M
⊢ False
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
⊢ ‖x + 1‖ ^ m ≤ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k

pp: R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
⊢ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k ≤ (m + 1) • max 1 (‖x‖ ^ m)

Tactic:
· 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 _ _)

Goal state after:
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
⊢ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k ≤ (m + 1) • max 1 (‖x‖ ^ m)
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: R : Type u_1
inst✝⁶ : SeminormedCommRing R
S : Type u_2
inst✝⁵ : Ring S
inst✝⁴ : Algebra R S
f✝ : AlgebraNorm R S
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra A S
inst✝ : IsScalarTower R A S
hinj : Function.Injective ⇑(algebraMap A S)
f : AlgebraNorm R S
x : A
hx : f ((algebraMap A S) x) = 0
⊢ x = 0

Tactic:
← map_eq_zero_iff (algebraMap A S) hinj

Goal state after:
R : Type u_1
inst✝⁶ : SeminormedCommRing R
S : Type u_2
inst✝⁵ : Ring S
inst✝⁴ : Algebra R S
f✝ : AlgebraNorm R S
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra A S
inst✝ : IsScalarTower R A S
hinj : Function.Injective ⇑(algebraMap A S)
f : AlgebraNorm R S
x : A
hx : f ((algebraMap A S) x) = 0
⊢ (algebraMap A S) x = 0
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝ : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx : f.toFun x = 0
c : K
hc : f c ≠ 0
hn0 : ¬x = 0
⊢ f (x * (c * x⁻¹)) = 0

Tactic:
exact
          le_antisymm
            (le_trans (map_mul_le_mul f _ _)
              (by rw [← RingSeminorm.toFun_eq_coe, ← AddGroupSeminorm.toFun_eq_coe, hx,
                zero_mul]))
            (apply_nonneg f _)

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
x : R
f_mul : 1 ≤ c * f 1
hx : 0 < f x
f_nonneg : 0 ≤ f 1
h1 : 0 < f 1
⊢ 0 ≤ c

Tactic:
rw [← div_le_iff₀ h1] at f_mul
        linarith [one_div_pos.mpr h1]

Goal state after: