mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
⊢ f 1 / f 1 ≤ ⨆ y, f y / f y

Tactic:
have h_bdd : BddAbove (Set.range fun y ↦ f y / f y) := by
      use (1 : ℝ)
      rintro r ⟨y, rfl⟩
      by_cases hy : f y = 0
      · simp only [hy, div_zero, zero_le_one]
      · simp only [div_self hy, le_refl]

Goal state after:
case a
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
h_bdd : BddAbove (Set.range fun y ↦ f y / f y)
⊢ f 1 / f 1 ≤ ⨆ y, f y / f y
Module: Mathlib.FieldTheory.Minpoly.IsConjRoot

Goal state before:
pp: R : Type u_1
A : Type u_5
B : Type u_6
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x y : A
f : A →ₐ[R] B
hf : Function.Injective ⇑f
⊢ IsConjRoot R (f x) (f y) ↔ IsConjRoot R x y

Tactic:
by
  rw [isConjRoot_def, isConjRoot_def, algHom_eq f hf, algHom_eq f hf]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝² : NormedAddCommGroup X
M : Type u_2
inst✝¹ : Ring M
inst✝ : Module M X
P : M
h : IsLprojection X P
x : X
⊢ ‖x‖ = ‖(1 - (1 - P)) • x‖ + ‖(1 - P) • x‖

Tactic:
sub_sub_cancel

Goal state after:
X : Type u_1
inst✝² : NormedAddCommGroup X
M : Type u_2
inst✝¹ : Ring M
inst✝ : Module M X
P : M
h : IsLprojection X P
x : X
⊢ ‖x‖ = ‖P • x‖ + ‖(1 - P) • x‖
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: ι : Type u_1
v : ι → ℝ
hv : Multipliable v
r₁ : ℝ
hr₁ : 0 < r₁ ∧ ∏' (i : ι), v i < r₁
this : ∀ᶠ (a : Finset ι) in { filter := atTop }.filter, ∏ b ∈ a, v b ≤ r₁
⊢ ∃ r₁ > 0, ∃ s₁, ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, v i ≤ r₁

Tactic:
eventually_atTop

Goal state after:
ι : Type u_1
v : ι → ℝ
hv : Multipliable v
r₁ : ℝ
hr₁ : 0 < r₁ ∧ ∏' (i : ι), v i < r₁
this : ∃ a, ∀ (b : Finset ι), a ⊆ b → ∏ b ∈ b, v b ≤ r₁
⊢ ∃ r₁ > 0, ∃ s₁, ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, v i ≤ r₁
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ (P ⊔ Q) ⊓ (P ⊔ R) ≤ P ⊔ Q ⊓ R

Tactic:
have e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * (R : M) * ↑Pᶜ := by
      rw [coe_inf, coe_sup, coe_sup, ← add_sub, ← add_sub, ← compl_mul, ← compl_mul, add_mul,
        mul_add, (Pᶜ.prop.commute Q.prop).eq, mul_add, ← mul_assoc, mul_assoc (Q : M),
        (Pᶜ.prop.commute P.prop).eq, mul_compl_self, zero_mul, mul_zero,
        zero_add, add_zero, ← mul_assoc, mul_assoc (Q : M), P.prop.proj.eq, Pᶜ.prop.proj.eq,
        mul_assoc, (Pᶜ.prop.commute R.prop).eq, ← mul_assoc]

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * ↑R * ↑Pᶜ
⊢ (P ⊔ Q) ⊓ (P ⊔ R) ≤ P ⊔ Q ⊓ R
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : NormedCommRing R
inst✝² : NormOneClass R
f : ι → R
inst✝¹ : CompleteSpace R
inst✝ : NormMulClass R
hf : ∀ (i : ι), 1 + f i ≠ 0
hu : Summable fun x ↦ ‖f x‖
⊢ ∏' (i : ι), (1 + f i) ≠ 0

Tactic:
by
  rw [← norm_ne_zero_iff, Multipliable.norm_tprod]
  · rw [← Real.rexp_tsum_eq_tprod (fun i ↦ norm_pos_iff.mpr <| hf i) hu.summable_log_norm_one_add]
    apply Real.exp_ne_zero
  · exact multipliable_one_add_of_summable hu

Goal state after:
Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn

Goal state before:
pp: α : Type u_1
ι : Type u_2
s✝ : Set α
f : ι → α → ℂ
hf : SummableUniformlyOn (fun i x ↦ log (f i x)) s✝
hfn : ∀ x ∈ s✝, ∀ (i : ι), f i x ≠ 0
hg : BddAbove ((fun x ↦ (∑' (i : ι), log (f i x)).re) '' s✝)
r : α → ℂ
hr : HasSumUniformlyOn (fun i x ↦ log (f i x)) r s✝
s : Finset ι
i : α
hi : i ∈ s✝
⊢ (cexp ∘ fun x2 ↦ ∑ i ∈ s, log (f i x2)) i = (fun x ↦ ∏ i ∈ s, f i x) i

Tactic:
simp [exp_sum, fun y ↦ exp_log (hfn i hi y)]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : Preorder α
inst✝¹ : IsOrderedMonoid α
inst✝ : ContinuousConstSMul α α
s : Set α
hs : IsOpen s
⊢ IsOpen ↑(upperClosure s)

Tactic:
by
    rw [← mul_one s, ← mul_upperClosure]
    exact hs.mul_right

Goal state after:
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: ι : Type u_2
inst✝ : Fintype ι
y y₁ : ι → ℝ
hy₁ : y₁ ∈ Ici y
y₂ : ι → ℝ
hy₂ : y₂ ∈ Ici y
hy : y₁ ≤ y₂
i : ι
x✝ : i ∈ Finset.univ
⊢ nndist (y₁ i) (y i) ≤ nndist (y₂ i) (y i)

Tactic:
rw [Real.nndist_eq, Real.nnabs_of_nonneg (sub_nonneg_of_le (‹y ≤ _› i : y i ≤ y₁ i)),
    Real.nndist_eq, Real.nnabs_of_nonneg (sub_nonneg_of_le (‹y ≤ _› i : y i ≤ y₂ i))]

Goal state after:
ι : Type u_2
inst✝ : Fintype ι
y y₁ : ι → ℝ
hy₁ : y₁ ∈ Ici y
y₂ : ι → ℝ
hy₂ : y₂ ∈ Ici y
hy : y₁ ≤ y₂
i : ι
x✝ : i ∈ Finset.univ
⊢ (y₁ i - y i).toNNReal ≤ (y₂ i - y i).toNNReal
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : NormedSpace 𝕜 V
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeparatingDual 𝕜 V
inst✝ : SeparatingDual 𝕜 W
f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →L[𝕜] W := (apply' W (RingHom.id 𝕜)) z ∘SL (↑f).toContinuousLinearMap ∘SL (smulRightL 𝕜 V V) v
hT : ∀ (x : V), T x = (f (smulRight v x)) z
this : ∀ (A : V →L[𝕜] V) (x : V), T (A x) = (f A) (T x)
d : StrongDual 𝕜 W
hd : d ((f (smulRight v u)) z) = 1
surj : Function.Surjective ⇑T
x y : V
hxy : T x = T y
w : V
⊢ (f.toAlgEquiv (smulRight v x)) (T w) = (f.toAlgEquiv (smulRight v y)) (T w)

Tactic:
simp [← this, hxy]

Goal state after:
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → E
K a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
ha : f a = 0
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ K * ‖f x‖
x : ℝ
hx : x ∈ Icc a b
⊢ gronwallBound 0 K 0 (x - a) = 0

Tactic:
by rw [gronwallBound_ε0_δ0]

Goal state after:
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: case refine_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → x ∈ closedBall x₀ ↑r → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : E → ℝ → E := fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
hα' : α' = fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
L' : ℝ≥0
h :
  ∀ (x y : E) (hx : x ∈ closedBall x₀ ↑r) (hy : y ∈ closedBall x₀ ↑r) (α β : FunSpace t₀ x₀ r L),
    IsFixedPt (FunSpace.next hf hx) α → IsFixedPt (FunSpace.next hf hy) β → dist α β ≤ ↑L' * dist x y
t : ℝ
ht : t ∈ Icc tmin tmax
x : E
hx : x ∈ closedBall x₀ ↑r
y : E
hy : y ∈ closedBall x₀ ↑r
⊢ dist ((α x hx).compProj t) ((if hx : y ∈ closedBall x₀ ↑r then (α y hx).compProj else 0) t) ≤ ↑L' * dist x y

Tactic:
dif_pos hy,

Goal state after:
case refine_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → x ∈ closedBall x₀ ↑r → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : E → ℝ → E := fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
hα' : α' = fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
L' : ℝ≥0
h :
  ∀ (x y : E) (hx : x ∈ closedBall x₀ ↑r) (hy : y ∈ closedBall x₀ ↑r) (α β : FunSpace t₀ x₀ r L),
    IsFixedPt (FunSpace.next hf hx) α → IsFixedPt (FunSpace.next hf hy) β → dist α β ≤ ↑L' * dist x y
t : ℝ
ht : t ∈ Icc tmin tmax
x : E
hx : x ∈ closedBall x₀ ↑r
y : E
hy : y ∈ closedBall x₀ ↑r
⊢ dist ((α x hx).compProj t) ((α y hy).compProj t) ≤ ↑L' * dist x y
Module: Mathlib.Analysis.Polynomial.Norm

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedRing A
p : A[X]
⊢ ∃ i, p.supNorm = ‖p.coeff i‖

Tactic:
simpa using! p.exists_eq_gaussNorm (SeminormedRing.toRingSeminorm A) 1

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

Goal state before:
pp: z : ℂ
⊢ (C z).logMahlerMeasure = log ‖z‖

Tactic:
by
  simp [logMahlerMeasure_def, circleAverage_def, mul_assoc]

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

Goal state before:
pp: n : ℕ
z : ℂ
⊢ ((monomial n) z).logMahlerMeasure = log ‖z‖

Tactic:
by
  simp [logMahlerMeasure_def, circleAverage_def, mul_assoc]

Goal state after:
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: r : ℝ
n : ℕ
hn : r < ↑n
⊢ ∀ᶠ (x : ℕ) in atTop, r < ↑x

Tactic:
eventually_atTop

Goal state after:
r : ℝ
n : ℕ
hn : r < ↑n
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → r < ↑b
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: ⊢ 3.141592 < π

Tactic:
pi_lower_bound [
    11482/8119, 7792/4217, 54055/27557, 2-623/64690, 2-337/139887, 2-208/345307, 2-167/1108925,
    2-64/1699893, 2-31/3293535, 2-48/20398657]

Goal state after:
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case refine_1
r : ℝ
f : ℕ → ℝ
H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun n ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun n ↦ i.2
s : ℝ
hs : s < r
⊢ ↑s ≤ ofSeq f

Tactic:
obtain ⟨t, ht⟩ := exists_gt r

Goal state after:
case refine_1
r : ℝ
f : ℕ → ℝ
H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun n ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun n ↦ i.2
s : ℝ
hs : s < r
t : ℝ
ht : r < t
⊢ ↑s ≤ ofSeq f
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case refine_3
b✝ n✝ b : ℕ
hb0 : 0 < ↑n✝ + 2
hb : 1 < ↑b
n : ℕ
x : ℕ → Fin b
⊢ ofDigitsTerm x n ≤ (↑b ^ n)⁻¹

Tactic:
apply ofDigitsTerm_le.trans

Goal state after:
case refine_3
b✝ n✝ b : ℕ
hb0 : 0 < ↑n✝ + 2
hb : 1 < ↑b
n : ℕ
x : ℕ → Fin b
⊢ (↑b - 1) * (↑b ^ (n + 1))⁻¹ ≤ (↑b ^ n)⁻¹
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
r : ℝ
hx : (∀ s < r, ↑s ≤ x) ∧ ∀ s > r, x ≤ ↑s
s : ℝ
hs : s < r
⊢ 0 ≤ ArchimedeanClass.mk x

Tactic:
obtain ⟨t, ht⟩ := exists_gt r

Goal state after:
x : ℝ*
r : ℝ
hx : (∀ s < r, ↑s ≤ x) ∧ ∀ s > r, x ≤ ↑s
s : ℝ
hs : s < r
t : ℝ
ht : r < t
⊢ 0 ≤ ArchimedeanClass.mk x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
⊢ tan z.arctan = z

Tactic:
unfold tan sin cos

Goal state after:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
⊢ (cexp (-z.arctan * I) - cexp (z.arctan * I)) * I / 2 / ((cexp (z.arctan * I) + cexp (-z.arctan * I)) / 2) = z
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: case succ
k : ℕ
hk : 0 < W k
⊢ 0 < W (k + 1)

Tactic:
rw [W_succ]

Goal state after:
case succ
k : ℕ
hk : 0 < W k
⊢ 0 < W k * ((2 * ↑k + 2) / (2 * ↑k + 1) * ((2 * ↑k + 2) / (2 * ↑k + 3)))
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ x ^ 2 - (x ^ 2 - 1) = 1

Tactic:
sub_sub_cancel

Goal state after:
x : ℝ
hx : 1 ≤ x
⊢ 1 = 1
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
⊢ (∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
have hu₂ (x) : HasDerivAt u₂ (u₂' x) x := by
    convert! (hasDerivAt_id' x).fun_mul ((hf x).fun_pow _) using 1
    simp only [u₂']
    ring

Goal state after:
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
⊢ (∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
h✝ : x < 1
⊢ artanh 0 ≤ artanh x

Tactic:
artanh_le_artanh_iff (by grind) (by grind)

Goal state after:
x : ℝ
hx : 0 ≤ x
h✝ : x < 1
⊢ 0 ≤ x
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ≤ 0
h✝ : -1 < x
⊢ artanh x ≤ artanh 0

Tactic:
artanh_le_artanh_iff (by grind) (by grind)

Goal state after:
x : ℝ
hx : x ≤ 0
h✝ : -1 < x
⊢ x ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: case inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : z.re ≤ |z.im|
⊢ ↑n * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖

Tactic:
have H : 1 < |z.im| := h₁.trans_le hle
            norm_cast at *
            rwa [max_eq_right hle, Real.norm_eq_abs, Real.norm_eq_abs, abs_of_pos (Real.log_pos H),
              ← Real.log_pow, Real.log_le_iff_le_exp (pow_pos (one_pos.trans H) _),
              abs_of_pos (one_pos.trans h₁)]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
m n : ℤ
⊢ (fun z ↦ z ^ m * cexp (↑b₁ * z)) =o[l] fun z ↦ z ^ n * cexp (↑b₂ * z)

Tactic:
simpa only [cpow_intCast] using hl.isLittleO_cpow_mul_exp hb m n

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt

Goal state before:
pp: A : Type u_1
inst✝¹⁰ : PartialOrder A
inst✝⁹ : Ring A
inst✝⁸ : StarRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarOrderedRing A
inst✝⁵ : Algebra ℝ A
inst✝⁴ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : SeparatelyContinuousMul A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
c a : A
hc : IsStrictlyPositive c
hc' : IsSelfAdjoint (sqrt c)
⊢ IsStrictlyPositive (sqrt c * a * sqrt c) ↔ IsStrictlyPositive a

Tactic:
by_cases ha : IsSelfAdjoint a

Goal state after:
case pos
A : Type u_1
inst✝¹⁰ : PartialOrder A
inst✝⁹ : Ring A
inst✝⁸ : StarRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarOrderedRing A
inst✝⁵ : Algebra ℝ A
inst✝⁴ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : SeparatelyContinuousMul A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
c a : A
hc : IsStrictlyPositive c
hc' : IsSelfAdjoint (sqrt c)
ha : IsSelfAdjoint a
⊢ IsStrictlyPositive (sqrt c * a * sqrt c) ↔ IsStrictlyPositive a

case neg
A : Type u_1
inst✝¹⁰ : PartialOrder A
inst✝⁹ : Ring A
inst✝⁸ : StarRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarOrderedRing A
inst✝⁵ : Algebra ℝ A
inst✝⁴ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : SeparatelyContinuousMul A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
c a : A
hc : IsStrictlyPositive c
hc' : IsSelfAdjoint (sqrt c)
ha : ¬IsSelfAdjoint a
⊢ IsStrictlyPositive (sqrt c * a * sqrt c) ↔ IsStrictlyPositive a
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
⊢ eval₂ (Int.castRingHom ℝ) (↑a / ↑b) (p.sum fun n a ↦ (monomial n) a) * ↑b ^ k =
    ↑(∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i))

Tactic:
eval₂_sum,

Goal state after:
case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
⊢ (p.sum fun n a_1 ↦ eval₂ (Int.castRingHom ℝ) (↑a / ↑b) ((monomial n) a_1)) * ↑b ^ k =
    ↑(∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i))
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
⊢ ∑ x ∈ p.support, ↑(p.coeff x) * (↑a ^ x / ↑b ^ x) * ↑b ^ k = ∑ x ∈ p.support, ↑(p.coeff x) * ↑a ^ x * ↑b ^ (k - x)

Tactic:
refine Finset.sum_congr rfl (fun i hi => ?_)

Goal state after:
case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
i : ℕ
hi : i ∈ p.support
⊢ ↑(p.coeff i) * (↑a ^ i / ↑b ^ i) * ↑b ^ k = ↑(p.coeff i) * ↑a ^ i * ↑b ^ (k - i)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: case neg
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
r : ℝ
hr : r ∈ spectrum ℝ z
ha' : ¬a = 0
⊢ 0 < a + b * r

Tactic:
· grind [add_pos_of_pos_of_nonneg, mul_nonneg]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ EqOn (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (fun t ↦ t ^ (p - 1) * x / (t + x)) (Ioi 0)

Tactic:
intro t ht
  simp [rpowIntegrand₀₁_eq_pow_div hp (le_of_lt ht) hx]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
⊢ p.rpowIntegrand₀₁ (x * t) x * x = p.rpowIntegrand₀₁ t 1 * x ^ p

Tactic:
by
  simp only [rpowIntegrand₀₁_apply_mul hp ht hx, mul_assoc]
  congr
  simpa using Eq.symm <| Real.rpow_add' hx (by aesop : (p - 1) + 1 ≠ 0)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm ((algebraMap ℝ A) t, LinearMap.id)
haddl : Function.Injective ⇑addl
hici : Ici 0 = ⇑addl ⁻¹' ⇑addl '' Ici 0
⊢ Ici ((algebraMap ℝ A) t) ⊆ {a | IsStrictlyPositive a}

Tactic:
exact fun x hx  => IsStrictlyPositive.of_le (by grind) hx

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case pos
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : x = 0
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)

pp: case neg
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)

Tactic:
case pos =>
    simp only [rpowIntegrand₀₁, hx_zero, add_zero, sub_self, mul_zero]
    positivity

Goal state after:
case neg
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: n : ℕ
⊢ eulerMascheroniConstant < eulerMascheroniSeq' n

Tactic:
refine lt_of_le_of_lt ?_ (strictAnti_eulerMascheroniSeq' (Nat.lt_succ_self n))

Goal state after:
n : ℕ
⊢ eulerMascheroniConstant ≤ eulerMascheroniSeq' n.succ
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ (fun x ↦ cexp (a * ↑x ^ 2 + b * ↑x)) =o[atTop] fun x ↦ x ^ s

Tactic:
apply Asymptotics.IsLittleO.of_norm_left

Goal state after:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ (fun x ↦ ‖cexp (a * ↑x ^ 2 + b * ↑x)‖) =o[atTop] fun x ↦ x ^ s
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
⊢ rexp ((a * ↑(x ^ 2)).re + (b * ↑x).re) = rexp (a.re * x ^ 2 + b.re * x)

Tactic:
mul_comm (_ : ℂ) ↑(_ : ℝ),

Goal state after:
a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
⊢ rexp ((↑(x ^ 2) * a).re + (↑x * b).re) = rexp (a.re * x ^ 2 + b.re * x)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: case e_a.e_a.e_a.refine_1
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ HasDerivAt (fun s ↦ 1 - s * 2) (-2) (1 / 2)

Tactic:
apply HasDerivAt.const_sub

Goal state after:
case e_a.e_a.e_a.refine_1
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ HasDerivAt (fun x ↦ x * 2) 2 (1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε y : ℝ
⊢ HasDerivAt ε.mulExpNegMulSq (rexp (-(ε * y * y)) + y * (rexp (-(ε * y * y)) * (-2 * ε * y))) y

Tactic:
nth_rw 1 [← one_mul (exp (-(ε * y * y)))]

Goal state after:
ε y : ℝ
⊢ HasDerivAt ε.mulExpNegMulSq (1 * rexp (-(ε * y * y)) + y * (rexp (-(ε * y * y)) * (-2 * ε * y))) y
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
hb₀ : 0 < b
hb : b ≠ 1
⊢ ContinuousAt (logb b) x ↔ x ≠ 0

Tactic:
refine ⟨?_, continuousAt_logb⟩
  rintro h rfl
  cases lt_or_gt_of_ne hb with
  | inl hb₁ =>
      exact not_tendsto_nhds_of_tendsto_atTop (tendsto_logb_nhdsNE_zero_of_base_lt_one hb₀ hb₁)
        _ (h.tendsto.mono_left inf_le_left)
  | inr hb₁ =>
      exact not_tendsto_nhds_of_tendsto_atBot (tendsto_logb_nhdsNE_zero hb₁)
        _ (h.tendsto.mono_left inf_le_left)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Goal state before:
pp: case h
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ (b : ℕ), N ≤ b → u b ∈ Set.Ioi 0
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(u n).mulExpNegMulSq (g ω)‖ ≤ ‖g‖

Tactic:
eventually_atTop

Goal state after:
case h
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ (b : ℕ), N ≤ b → u b ∈ Set.Ioi 0
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → ∀ᵐ (ω : E) ∂P, ‖(u b).mulExpNegMulSq (g ω)‖ ≤ ‖g‖
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Goal state before:
pp: case h
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) ω‖ ≤ ‖g‖

Tactic:
eventually_atTop

Goal state after:
case h
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → ∀ᵐ (ω : E) ∂P, ‖(g * (1 + (↑b)⁻¹ • -(ε • g * g)) ^ b) ω‖ ≤ ‖g‖