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

Goal state before:
pp: case inl.inr.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
h : HolderOnWith 0 r f s
x : X
hx : x ∈ s
this : f '' s = {f x}
hd : 0 ≤ 0
⊢ μH[0] {f x} ≤ ↑0 ^ 0 * μH[↑r * 0] s

Tactic:
simp only [ENNReal.rpow_zero, one_mul, mul_zero]
      rw [hausdorffMeasure_zero_singleton]
      exact one_le_hausdorffMeasure_zero_of_nonempty ⟨x, hx⟩

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
inst✝ : TopologicalSpace α
f : α → E →WOT[𝕜] F
s : Set α
⊢ ContinuousOn f s ↔ ∀ (x : E) (y : F), ContinuousOn (fun x_1 ↦ ⟪y, (f x_1) x⟫_𝕜) s

Tactic:
ContinuousOn,

Goal state after:
𝕜 : 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
inst✝ : TopologicalSpace α
f : α → E →WOT[𝕜] F
s : Set α
⊢ (∀ x ∈ s, ContinuousWithinAt f s x) ↔
    ∀ (x : E) (y : F), ∀ x_1 ∈ s, ContinuousWithinAt (fun x_2 ↦ ⟪y, (f x_2) x⟫_𝕜) s x_1
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
⊢ μH[d] (⇑(AffineMap.homothety x c) '' s) = ‖c‖₊ ^ d • μH[d] s

Tactic:
suffices
    μH[d] (IsometryEquiv.vaddConst x '' (c • ·) '' (IsometryEquiv.vaddConst x).symm '' s) =
      ‖c‖₊ ^ d • μH[d] s by
    simpa only [Set.image_image]
  borelize E
  rw [IsometryEquiv.hausdorffMeasure_image, Set.image_smul, Measure.hausdorffMeasure_smul₀ hd hc,
    IsometryEquiv.hausdorffMeasure_image]

Goal state after:
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)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x y : E
⊢ (o.kahler (φ x)) (φ y) = (o.kahler x) y

Tactic:
simp [kahler_apply_apply, o.areaForm_comp_linearIsometryEquiv φ hφ]

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)⁻¹
t : ℝ
ht : t ∈ Set.Icc 0 1
⊢ HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)

Tactic:
rw [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)⁻¹
t : ℝ
ht : t ∈ Set.Icc 0 1
⊢ HasDerivAt f (f' (↑t * z)) (↑t * z)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun y ↦ y * (2 * z)) (2 * z) ↑x
⊢ HasDerivAt (fun y ↦ Complex.sin (2 * z * ↑y) / (2 * z)) (Complex.cos (2 * z * ↑x)) x

Tactic:
have b : HasDerivAt (Complex.sin ∘ fun y : ℂ => (y * (2 * z))) _ x :=
    HasDerivAt.comp (x : ℂ) (Complex.hasDerivAt_sin (x * (2 * z))) a

Goal state after:
z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun y ↦ y * (2 * z)) (2 * z) ↑x
b : HasDerivAt (Complex.sin ∘ fun y ↦ y * (2 * z)) (Complex.cos (↑x * (2 * z)) * (2 * z)) ↑x
⊢ HasDerivAt (fun y ↦ Complex.sin (2 * z * ↑y) / (2 * z)) (Complex.cos (2 * z * ↑x)) x
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
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
⊢ ContinuousOn (fun t ↦ ↑(log t)) (Ioi 0)

Tactic:
refine continuous_ofReal.comp_continuousOn ?_

Goal state after:
case refine_2
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
⊢ ContinuousOn log (Ioi 0)
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 ∈ Metric.ball s v
h : 1 ≤ t
⊢ z.re - re 1 ≤ s.re + v - 1

Tactic:
one_re,

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 ∈ Metric.ball s v
h : 1 ≤ t
⊢ z.re - 1 ≤ s.re + v - 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case hf
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ -1 < u.re - re 1

Tactic:
one_re,

Goal state after:
case hf
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ -1 < u.re - 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case hg
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
⊢ ↑(1 - x) ∈ slitPlane

Tactic:
exact ofReal_mem_slitPlane.2 <| by linarith only [hx.2]

Goal state after:
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 : z ∈ Metric.ball s v
h : t < 1
⊢ s.re - v - 1 ≤ z.re - re 1

Tactic:
one_re,

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 : z ∈ Metric.ball s v
h : t < 1
⊢ s.re - v - 1 ≤ z.re - 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: u : ℂ
hu : 0 < u.re
⊢ -1 < u.re - re 1

Tactic:
one_re,

Goal state after:
u : ℂ
hu : 0 < u.re
⊢ -1 < u.re - 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) ∂volume =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1) ∂volume) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1) ∂volume
⊢ 0 < s.re + t.re

Tactic:
exact add_pos hs ht

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

Goal state before:
pp: s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) ∂volume =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1) ∂volume) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1) ∂volume
hst : 0 < (s + t).re
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
this : cexp (-↑x) = cexp (-↑y) * cexp (-(↑x - ↑y))
⊢ cexp (-↑y) * ↑y ^ (s - 1) * (cexp (-(↑x - ↑y)) * (↑x - ↑y) ^ (t - 1)) =
    cexp (-↑x) * (↑y ^ (s - 1) * (↑x - ↑y) ^ (t - 1))

Tactic:
by rw [this]; ring

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

Goal state before:
pp: case refine_2
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x ↦ ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
x : ℝ
hx : x ∈ Icc 0 1
⊢ 0 ≤ re 1 - (↑x).re

Tactic:
one_re,

Goal state after:
case refine_2
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x ↦ ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
x : ℝ
hx : x ∈ Icc 0 1
⊢ 0 ≤ 1 - (↑x).re
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case refine_1
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x ↦ ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y ↦ y ^ u) (u * ↑x ^ (u - 1)) ↑x
⊢ 0 < re 1 - (↑x).re

Tactic:
one_re,

Goal state after:
case refine_1
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x ↦ ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y ↦ y ^ u) (u * ↑x ^ (u - 1)) ↑x
⊢ 0 < 1 - (↑x).re
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
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Tactic:
suffices ∀ m : ℕ, ↑m < x → x ≤ m + 1 → Tendsto (logGammaSeq x) atTop (𝓝 <| f x - f 1) 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:
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
⊢ ∀ (m : ℕ), ↑m < x → x ≤ ↑m + 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f g : 𝕜 → 𝕜'
U : Set 𝕜
hf : MeromorphicOn f U
hg : MeromorphicOn g U
h'f : ∀ x ∈ U, meromorphicOrderAt f x ≠ ⊤
h'g : ∀ x ∈ U, meromorphicOrderAt g x ≠ ⊤
y : 𝕜
h₁y : AnalyticAt 𝕜 f y
h₂y : AnalyticAt 𝕜 g y
h₃y : f y ≠ 0
h₄y : g y ≠ 0
⊢ logDeriv (f * g) y = logDeriv f y + logDeriv g y

Tactic:
Pi.mul_def

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f g : 𝕜 → 𝕜'
U : Set 𝕜
hf : MeromorphicOn f U
hg : MeromorphicOn g U
h'f : ∀ x ∈ U, meromorphicOrderAt f x ≠ ⊤
h'g : ∀ x ∈ U, meromorphicOrderAt g x ≠ ⊤
y : 𝕜
h₁y : AnalyticAt 𝕜 f y
h₂y : AnalyticAt 𝕜 g y
h₃y : f y ≠ 0
h₄y : g y ≠ 0
⊢ logDeriv (fun i ↦ f i * g i) y = logDeriv f y + logDeriv g y
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case zero
u : ℂ
hu : 0 < u.re
⊢ 1 / u = ↑0! / ∏ j ∈ Finset.range (0 + 1), (u + ↑j)

Tactic:
Nat.factorial_zero,

Goal state after:
case zero
u : ℂ
hu : 0 < u.re
⊢ 1 / u = ↑1 / ∏ j ∈ Finset.range (0 + 1), (u + ↑j)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: s : ℝ
hs : 0 < s
⊢ s.doublingGamma = Γ s

Tactic:
refine
    eq_Gamma_of_log_convex doublingGamma_log_convex_Ioi
      (fun {y} hy => doublingGamma_add_one y hy.ne') (fun {y} hy => ?_) doublingGamma_one hs
  apply_rules [mul_pos, Gamma_pos_of_pos, add_pos, inv_pos_of_pos, rpow_pos_of_pos, two_pos,
    one_pos, sqrt_pos_of_pos 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
inst✝ : FiniteDimensional ℝ V
s : Set P
h : asymptoticCone ℝ s ⊆ {0}
⊢ Bornology.IsBounded s

Tactic:
simp_rw [isBounded_def, cobounded_eq_iSup_sphere_asymptoticNhds, mem_iSup]

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set P
h : asymptoticCone ℝ s ⊆ {0}
⊢ ∀ i ∈ Metric.sphere 0 1, sᶜ ∈ asymptoticNhds ℝ P i
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case hf
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
n : ℕ
⊢ -1 < s.re - re 1

Tactic:
one_re,

Goal state after:
case hf
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
n : ℕ
⊢ -1 < s.re - 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: n : ℕ
ihn : ∀ (s : ℂ), -s.re < ↑n → DifferentiableAt ℂ (fun s ↦ (Gamma s)⁻¹) s
s : ℂ
hs : -s.re < ↑(n + 1)
⊢ -(s.re + re 1) < ↑n

Tactic:
one_re,

Goal state after:
n : ℕ
ihn : ∀ (s : ℂ), -s.re < ↑n → DifferentiableAt ℂ (fun s ↦ (Gamma s)⁻¹) s
s : ℂ
hs : -s.re < ↑(n + 1)
⊢ -(s.re + 1) < ↑n
Module: Mathlib.Analysis.Normed.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : Algebra ℚ R
inst✝² : UniformSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
r : R
⊢ exp (r • ε) = 1 + r • ε

Tactic:
by
  rw [eps, ← inr_smul, exp_inr]

Goal state after:
Module: Mathlib.Analysis.Polynomial.Factorization

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : IsAlgClosed F
f : F[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
f₁ : F[X]
hf₁m : f₁.Monic
hf₁i : Irreducible f₁
f₂ : F[X]
hf₂ : f = f₁ * f₂
⊢ ∃ f₁ f₂, f₁.IsMonicOfDegree 1 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂

Tactic:
rw [hf₂, add_comm] at hf

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : IsAlgClosed F
f : F[X]
n : ℕ
f₁ : F[X]
hf₁m : f₁.Monic
hf₁i : Irreducible f₁
f₂ : F[X]
hf : (f₁ * f₂).IsMonicOfDegree (1 + n)
hf₂ : f = f₁ * f₂
⊢ ∃ f₁ f₂, f₁.IsMonicOfDegree 1 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁶ : Field 𝕜
inst✝¹⁵ : CharZero 𝕜
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Algebra 𝕜 R
inst✝¹¹ : Module 𝕜 M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower 𝕜 R M
inst✝⁶ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : IsTopologicalRing R
inst✝² : IsTopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
e : R
h : HasSum (fun n ↦ (↑n.factorial)⁻¹ • x.fst ^ n) e
⊢ HasSum (fun n ↦ ((↑n.factorial)⁻¹ • x.fst ^ n) • x.snd) (e • x.snd - ((↑(Nat.factorial 0))⁻¹ • x ^ 0).snd)

Tactic:
Nat.factorial_zero,

Goal state after:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁶ : Field 𝕜
inst✝¹⁵ : CharZero 𝕜
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Algebra 𝕜 R
inst✝¹¹ : Module 𝕜 M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower 𝕜 R M
inst✝⁶ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : IsTopologicalRing R
inst✝² : IsTopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
e : R
h : HasSum (fun n ↦ (↑n.factorial)⁻¹ • x.fst ^ n) e
⊢ HasSum (fun n ↦ ((↑n.factorial)⁻¹ • x.fst ^ n) • x.snd) (e • x.snd - ((↑1)⁻¹ • x ^ 0).snd)
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
⊢ ‖φ x u‖ ≤ M * (1 + (‖φ x u - φ x w‖ / M) ^ n)

Tactic:
have HH : M * (1 + (‖φ x u - φ x w‖ / M) ^ n) = (M ^ n + ‖φ x u - φ x w‖ ^ n) / M ^ (n - 1) := by
    simp only [field, div_pow, ← pow_succ', Nat.sub_add_cancel hn]

Goal state after:
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
HH : M * (1 + (‖φ x u - φ x w‖ / M) ^ n) = (M ^ n + ‖φ x u - φ x w‖ ^ n) / M ^ (n - 1)
⊢ ‖φ x u‖ ≤ M * (1 + (‖φ x u - φ x w‖ / M) ^ n)
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: F : Type u_2
α : Type u_3
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f : F
a : α
x✝ : 1 ≠ 0
⊢ f (a ^ 1) ≤ f a ^ 1

Tactic:
by simp only [pow_one, le_refl]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : f (x * 1) ≤ f x * f 1
h_one : f 1 ≤ 1
h_bdd : BddAbove (Set.range fun y ↦ f (x * y) / f y)
h0 : ¬f x = 0
⊢ 1 ≤ f 1

Tactic:
rw [mul_one, le_mul_iff_one_le_right (lt_of_le_of_ne (f_nonneg _) (Ne.symm h0))] at hx

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : 1 ≤ f 1
h_one : f 1 ≤ 1
h_bdd : BddAbove (Set.range fun y ↦ f (x * y) / f y)
h0 : ¬f x = 0
⊢ 1 ≤ f 1
Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : NormedField K
inst✝¹ : Field L
inst✝ : Algebra K L
hfd : FiniteDimensional K L
hna : IsNonarchimedean norm
h1 : LinearIndepOn K id {1}
ι : Type u_2 := { x // x ∈ h1.extend ⋯ }
B : Basis ι K L := Basis.extend h1
hfin : Fintype ι := FiniteDimensional.fintypeBasisIndex B
hem : Nonempty ι
h1L : 1 ∈ h1.extend ⋯
hB1 : B ⟨1, h1L⟩ = 1
g : L → ℝ := B.norm
hg0 : g 0 = 0
hg_nonneg : ∀ (x : L), 0 ≤ g x
hg_ext : ∀ (x : K), g ((algebraMap K L) x) = ‖x‖
hg_na : IsNonarchimedean g
hg_add : ∀ (a b : L), g (a + b) ≤ g a + g b
hg_neg : ∀ (a : L), g (-a) = g a
w✝¹ : ℝ
w✝ : 0 < w✝¹
hg_bdd : ∀ (x y : L), B.norm (x * y) ≤ w✝¹ * B.norm x * B.norm y
hg_mul : ∀ (k : K) (y : L), g ((algebraMap K L) k * y) = g ((algebraMap K L) k) * g y
f : RingSeminorm L := seminormFromBounded hg0 hg_nonneg hg_bdd hg_add hg_neg
hf_na : IsNonarchimedean ⇑f
hf_1 : f 1 ≤ 1
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖
F' : RingSeminorm L := smoothingSeminorm f hf_1 hf_na
hF' : F' = smoothingSeminorm f hf_1 hf_na
hF'_ext : ∀ (k : K), F' ((algebraMap K L) k) = ‖k‖
hF'_1 : F' 1 = 1
hF'_0 : F' ≠ 0
k : K
y : L
hk : ∀ (y : L), f ((algebraMap K L) k * y) = f ((algebraMap K L) k) * f y
⊢ (F'.toRingNorm hF'_0).toFun (k • y) = ‖k‖ * (F'.toRingNorm hF'_0).toFun y

Tactic:
have hfk : ‖k‖ = (smoothingSeminorm f hf_1 hf_na) ((algebraMap K L) k) := by
          rw [← hf_ext k, eq_comm, smoothingSeminorm_apply_of_map_mul_eq_mul f hf_1 hf_na hk]

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : NormedField K
inst✝¹ : Field L
inst✝ : Algebra K L
hfd : FiniteDimensional K L
hna : IsNonarchimedean norm
h1 : LinearIndepOn K id {1}
ι : Type u_2 := { x // x ∈ h1.extend ⋯ }
B : Basis ι K L := Basis.extend h1
hfin : Fintype ι := FiniteDimensional.fintypeBasisIndex B
hem : Nonempty ι
h1L : 1 ∈ h1.extend ⋯
hB1 : B ⟨1, h1L⟩ = 1
g : L → ℝ := B.norm
hg0 : g 0 = 0
hg_nonneg : ∀ (x : L), 0 ≤ g x
hg_ext : ∀ (x : K), g ((algebraMap K L) x) = ‖x‖
hg_na : IsNonarchimedean g
hg_add : ∀ (a b : L), g (a + b) ≤ g a + g b
hg_neg : ∀ (a : L), g (-a) = g a
w✝¹ : ℝ
w✝ : 0 < w✝¹
hg_bdd : ∀ (x y : L), B.norm (x * y) ≤ w✝¹ * B.norm x * B.norm y
hg_mul : ∀ (k : K) (y : L), g ((algebraMap K L) k * y) = g ((algebraMap K L) k) * g y
f : RingSeminorm L := seminormFromBounded hg0 hg_nonneg hg_bdd hg_add hg_neg
hf_na : IsNonarchimedean ⇑f
hf_1 : f 1 ≤ 1
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖
F' : RingSeminorm L := smoothingSeminorm f hf_1 hf_na
hF' : F' = smoothingSeminorm f hf_1 hf_na
hF'_ext : ∀ (k : K), F' ((algebraMap K L) k) = ‖k‖
hF'_1 : F' 1 = 1
hF'_0 : F' ≠ 0
k : K
y : L
hk : ∀ (y : L), f ((algebraMap K L) k * y) = f ((algebraMap K L) k) * f y
hfk : ‖k‖ = (smoothingSeminorm f hf_1 hf_na) ((algebraMap K L) k)
⊢ (F'.toRingNorm hF'_0).toFun (k • y) = ‖k‖ * (F'.toRingNorm hF'_0).toFun y
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x y : R
hlim : Tendsto (fun n ↦ seminormFromConst_seq c f (x * y) (2 * n)) atTop (𝓝 (seminormFromConst' c f (x * y)))
n : ℕ
⊢ f (x * y * c ^ n * c ^ n) ≤ f (x * c ^ n) * f (y * c ^ n)

Tactic:
mul_comm (x * y),

Goal state after:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x y : R
hlim : Tendsto (fun n ↦ seminormFromConst_seq c f (x * y) (2 * n)) atTop (𝓝 (seminormFromConst' c f (x * y)))
n : ℕ
⊢ f (c ^ n * (x * y) * c ^ n) ≤ f (x * c ^ n) * f (y * c ^ n)
Module: Mathlib.FieldTheory.Minpoly.IsConjRoot

Goal state before:

Tactic:
_ ↔ 2 ≤ (minpoly K x).natDegree := (minpoly.two_le_natDegree_iff h.isIntegral).symm
    _ ↔ 2 ≤ Fintype.card ((minpoly K x).rootSet L) :=
      (Polynomial.card_rootSet_eq_natDegree h sp) ▸ Iff.rfl
    _ ↔ Nontrivial ((minpoly K x).rootSet L) := Fintype.one_lt_card_iff_nontrivial
    _ ↔ ∃ y : ((minpoly K x).rootSet L), ↑y ≠ x :=
      (nontrivial_iff_exists_ne ⟨x, mem_rootSet.mpr ⟨minpoly.ne_zero h.isIntegral,
          minpoly.aeval K x⟩⟩).trans ⟨fun ⟨y, hy⟩ => ⟨y, Subtype.coe_ne_coe.mpr hy⟩,
          fun ⟨y, hy⟩ => ⟨y, Subtype.coe_ne_coe.mp hy⟩⟩
    _ ↔ _ :=
      ⟨fun ⟨⟨y, hy⟩, hne⟩ => ⟨y, ⟨hne.symm,
          (isConjRoot_iff_mem_minpoly_rootSet h.isIntegral).mpr hy⟩⟩,
          fun ⟨y, hne, hy⟩ => ⟨⟨y,
          (isConjRoot_iff_mem_minpoly_rootSet h.isIntegral).mp hy⟩, hne.symm⟩⟩

Goal state after: