mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 ≤ z ↔ ∃ x ≥ 0, ↑x = z

Tactic:
by
  simp_rw [nonneg_iff (K := K), ext_iff (K := K)]; aesop

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
y z : K
r : ℝ
hx : 0 ≤ re ↑r ∧ im ↑r = 0
hyz : r * re y < r * re z ∧ (im y = im z ∨ r = 0)
⊢ 0 ≤ r

Tactic:
simpa using hx

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : f =O[l] g
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
rw [isBigO_iff] at h
    obtain ⟨c, hc⟩ := h
    refine ⟨max c 1, zero_lt_one.trans_le (le_max_right _ _), ?_⟩
    filter_upwards [hc] with x hx
    apply hx.trans
    gcongr
    exact le_max_left _ _

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
⊢ f'' =o[𝓟 s] g' ↔ ∀ x ∈ s, f'' x = 0

Tactic:
refine ⟨fun h x hx ↦ norm_le_zero_iff.1 ?_, fun h ↦ ?_⟩
  · simp only [isLittleO_iff] at h
    have : Tendsto (fun c : ℝ => c * ‖g' x‖) (𝓝[>] 0) (𝓝 0) :=
      ((continuous_id.mul continuous_const).tendsto' _ _ (zero_mul _)).mono_left
        inf_le_left
    apply le_of_tendsto_of_tendsto tendsto_const_nhds this
    apply eventually_nhdsWithin_iff.2 (Eventually.of_forall (fun c hc ↦ ?_))
    exact eventually_principal.1 (h hc) x hx
  · apply (isLittleO_zero g' _).congr' ?_ EventuallyEq.rfl
    exact fun x hx ↦ (h x hx).symm

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
h₃ :
  ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k
two_mul_two : 4 = 2 * 2
hQ0 : Q ≠ 0
h2Q0 : 2 * Q ≠ 0
hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε
⊢ max N M + 1 < 2 * (max N M + 1)

Tactic:
by rw [two_mul]; exact lt_add_of_pos_left _ (Nat.succ_pos _)

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
⊢ ‖(exp' x).lim - (const norm (∑ m ∈ range n, x ^ m / ↑m.factorial)).lim‖ ≤ ‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹)

Tactic:
sub_eq_add_neg,

Goal state after:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
⊢ ‖(exp' x).lim + -(const norm (∑ m ∈ range n, x ^ m / ↑m.factorial)).lim‖ ≤ ‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
⊢ ‖(exp' x).lim - (const norm (∑ m ∈ range n, x ^ m / ↑m.factorial)).lim‖ ≤ ‖x‖ ^ n / ↑n.factorial * 2

Tactic:
sub_eq_add_neg,

Goal state after:
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
⊢ ‖(exp' x).lim + -(const norm (∑ m ∈ range n, x ^ m / ↑m.factorial)).lim‖ ≤ ‖x‖ ^ n / ↑n.factorial * 2
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
f : α → E
g'' : α → F''
h : f =O[cofinite] g''
C : ℝ
C₀ : C > 0
hC : {x | ¬‖f x‖ ≤ C * ‖g'' x‖}.Finite
C' : ℝ
hC' : ∀ i ∈ Finset.image (fun x ↦ ‖f x‖ / ‖g'' x‖) hC.toFinset, i ≤ C'
this : ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'
⊢ ∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖

Tactic:
refine ⟨max C C', lt_max_iff.2 (Or.inl C₀), fun x h₀ => ?_⟩

Goal state after:
α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
f : α → E
g'' : α → F''
h : f =O[cofinite] g''
C : ℝ
C₀ : C > 0
hC : {x | ¬‖f x‖ ≤ C * ‖g'' x‖}.Finite
C' : ℝ
hC' : ∀ i ∈ Finset.image (fun x ↦ ‖f x‖ / ‖g'' x‖) hC.toFinset, i ≤ C'
this : ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'
x : α
h₀ : g'' x ≠ 0
⊢ ‖f x‖ ≤ max C C' * ‖g'' x‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n : ℕ
⊢ ‖(exp' x).lim - (const norm (∑ m ∈ range n, x ^ m / ↑m.factorial)).lim‖ ≤
    Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / ↑m.factorial

Tactic:
sub_eq_add_neg,

Goal state after:
x : ℂ
n : ℕ
⊢ ‖(exp' x).lim + -(const norm (∑ m ∈ range n, x ^ m / ↑m.factorial)).lim‖ ≤
    Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / ↑m.factorial
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n : ℕ
⊢ ‖(exp' x).lim - (const norm (∑ m ∈ range n, x ^ m / ↑m.factorial)).lim‖ ≤ ‖x‖ ^ n * Real.exp ‖x‖

Tactic:
sub_eq_add_neg,

Goal state after:
x : ℂ
n : ℕ
⊢ ‖(exp' x).lim + -(const norm (∑ m ∈ range n, x ^ m / ↑m.factorial)).lim‖ ≤ ‖x‖ ^ n * Real.exp ‖x‖
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ abv x ^ n ≤ 1

Tactic:
exact pow_le_one₀ (by positivity) hx1.le

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

Goal state before:
pp: ⊢ Continuous sin

Tactic:
change Continuous fun z => (exp (-z * I) - exp (z * I)) * I / 2
  fun_prop

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁸ : SeminormedAddCommGroup M
inst✝⁷ : SeminormedAddCommGroup N
R : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : Module R M
S T : Submodule R M
𝕜 : Type u_4
inst✝⁴ : SeminormedCommRing 𝕜
inst✝³ : Module 𝕜 M
inst✝² : IsBoundedSMul 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
k : 𝕜
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
a : M
h : ∀ (x : ℝ), x - ‖mk a‖ < δ ∧ ‖mk a‖ - x < δ → ‖k‖ * x - ‖k‖ * ‖mk a‖ < ε ∧ ‖k‖ * ‖mk a‖ - ‖k‖ * x < ε
ha : ‖a‖ < ‖mk a‖ + δ
⊢ ‖k • mk a‖ ≤ ‖k‖ * ‖mk a‖ + ε

Tactic:
specialize h ‖a‖ ⟨by linarith, by linarith [Submodule.Quotient.norm_mk_le S a]⟩

Goal state after:
M : Type u_1
N : Type u_2
inst✝⁸ : SeminormedAddCommGroup M
inst✝⁷ : SeminormedAddCommGroup N
R : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : Module R M
S T : Submodule R M
𝕜 : Type u_4
inst✝⁴ : SeminormedCommRing 𝕜
inst✝³ : Module 𝕜 M
inst✝² : IsBoundedSMul 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
k : 𝕜
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
a : M
h : ‖k‖ * ‖a‖ - ‖k‖ * ‖mk a‖ < ε ∧ ‖k‖ * ‖mk a‖ - ‖k‖ * ‖a‖ < ε
ha : ‖a‖ < ‖mk a‖ + δ
⊢ ‖k • mk a‖ ≤ ‖k‖ * ‖mk a‖ + ε
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ √((1 + cos (π / 2 ^ (n + 1))) / 2) = sqrtTwoAddSeries 0 (n + 1) / 2

pp: case hl
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ -π ≤ π / 2 ^ (n + 1)

pp: case hr
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ π / 2 ^ (n + 1) ≤ π

Tactic:
cos_pi_over_two_pow n,

Goal state after:
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ √((1 + sqrtTwoAddSeries 0 n / 2) / 2) = sqrtTwoAddSeries 0 (n + 1) / 2

case hl
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ -π ≤ π / 2 ^ (n + 1)

case hr
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ π / 2 ^ (n + 1) ≤ π
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_2
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
⊢ (fun n ↦ ↑n ^ k * r₁ ^ n) =o[atTop] fun n ↦ r₂ ^ n

Tactic:
by
  by_cases h0 : r₁ = 0
  · refine (isLittleO_zero _ _).congr' (mem_atTop_sets.2 <| ⟨1, fun n hn ↦ ?_⟩) EventuallyEq.rfl
    simp [zero_pow (one_le_iff_ne_zero.1 hn), h0]
  rw [← Ne, ← norm_pos_iff] at h0
  have A : (fun n ↦ (n : R) ^ k : ℕ → R) =o[atTop] fun n ↦ (r₂ / ‖r₁‖) ^ n :=
    isLittleO_pow_const_const_pow_of_one_lt k ((one_lt_div h0).2 h)
  suffices (fun n ↦ r₁ ^ n) =O[atTop] fun n ↦ ‖r₁‖ ^ n by
    simpa [div_mul_cancel₀ _ (pow_pos h0 _).ne', div_pow] using A.mul_isBigO this
  exact .of_norm_eventuallyLE <| eventually_norm_pow_le r₁

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

Goal state before:
pp: case pos
R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n ↦ x ^ n
⊢ ‖1 + ∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Tactic:
refine le_trans (norm_add_le _ _) ?_

Goal state after:
case pos
R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n ↦ x ^ n
⊢ ‖1‖ + ‖∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n ↦ ↑(u n)) =O[atTop] fun n ↦ ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ (fun n ↦ ‖↑(u n) * r ^ n‖) =O[atTop] fun n ↦ r' ^ n

Tactic:
calc
  fun n ↦ ‖↑(u n) * r ^ n‖
  _ =O[atTop] fun n ↦ u n * ‖r‖ ^ n := by
      apply (IsBigOWith.of_bound (c := ‖(1 : R)‖) ?_).isBigO
      filter_upwards [eventually_norm_pow_le r] with n hn
      simp only [norm_mul, Real.norm_eq_abs, abs_cast, norm_pow, abs_norm]
      apply (norm_mul_le _ _).trans
      have : ‖(u n : R)‖ * ‖r ^ n‖ ≤ (u n * ‖(1 : R)‖) * ‖r‖ ^ n := by
        gcongr; exact norm_cast_le (u n)
      exact this.trans (le_of_eq (by ring))
  _ =O[atTop] fun n ↦ ↑(n ^ k) * ‖r‖ ^ n := hu.mul (isBigO_refl _ _)
  _ =O[atTop] fun n ↦ r' ^ n := by
      simp only [cast_pow]
      exact (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt k hrr').isBigO

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
a b : E
⊢ Metric.ball a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)

Tactic:
sub_eq_add_neg,

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
a b : E
⊢ Metric.ball a ε + -Metric.ball b δ = Metric.ball (a + -b) (ε + δ)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.ball a ε - Metric.closedBall b δ = Metric.ball (a - b) (ε + δ)

Tactic:
sub_eq_add_neg,

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.ball a ε + -Metric.closedBall b δ = Metric.ball (a + -b) (ε + δ)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
a b : E
⊢ Metric.closedBall a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)

Tactic:
sub_eq_add_neg,

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
a b : E
⊢ Metric.closedBall a ε + -Metric.ball b δ = Metric.ball (a + -b) (ε + δ)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
δ ε : ℝ
inst✝ : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.closedBall a ε - Metric.closedBall b δ = Metric.closedBall (a - b) (ε + δ)

Tactic:
sub_eq_add_neg,

Goal state after:
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
δ ε : ℝ
inst✝ : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.closedBall a ε + -Metric.closedBall b δ = Metric.closedBall (a - b) (ε + δ)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ Function.Periodic sinh (2 * ↑π * I)

Tactic:
convert! sinh_antiperiodic.periodic_two_mul using 1

Goal state after:
case e'_5
⊢ 2 * ↑π * I = 2 * (↑π * I)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case pos
α : Type u_1
inst✝ : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n ↦ if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ n ≥ N, u n = v n
n : ℕ
H : n < N
⊢ ‖0‖ ≤ C * r ^ n

Tactic:
rw [norm_zero]
    exact mul_nonneg hC (pow_nonneg hr₀.le _)

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

Goal state before:
pp: α : Type u_4
inst✝¹ : NormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
l : ℝ
hl₁ : l < 1
hf : ∀ᶠ (n : ℕ) in atTop, f n ≠ 0
h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
⊢ Summable f

Tactic:
rcases exists_between hl₁ with ⟨r, hr₀, hr₁⟩

Goal state after:
α : Type u_4
inst✝¹ : NormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
l : ℝ
hl₁ : l < 1
hf : ∀ᶠ (n : ℕ) in atTop, f n ≠ 0
h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
r : ℝ
hr₀ : l < r
hr₁ : r < 1
⊢ Summable f
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝ : PathConnectedSpace X
x : X
_x_in : x ∈ univ
hx : pathComponentIn univ x = univ
⊢ pathComponent x = univ

Tactic:
simpa using hx

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

Goal state before:
pp: E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n ↦
    f (n.succ - 1) • ∑ i ∈ Finset.range n.succ, z i -
      ∑ i ∈ Finset.range (n.succ - 1), (f (i + 1) - f i) • ∑ i ∈ Finset.range (i + 1), z i

Tactic:
sub_eq_add_neg,

Goal state after:
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n ↦
    f (n.succ - 1) • ∑ i ∈ Finset.range n.succ, z i +
      -∑ x ∈ Finset.range (n.succ - 1), (f (x + 1) + -f x) • ∑ i ∈ Finset.range (x + 1), z i
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < |p| / 2 then closedBall x ε ∩ s else s

Tactic:
rcases le_or_gt (|p| / 2) ε with hε | hε

Goal state after:
case inl
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : |p| / 2 ≤ ε
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < |p| / 2 then closedBall x ε ∩ s else s

case inr
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : ε < |p| / 2
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < |p| / 2 then closedBall x ε ∩ s else s
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case pos
x : ℂ
hx : x ≠ 0
h₁ : 0 ≤ x.re
⊢ ‖x‖ * √((‖x‖ ^ 2 - x.im ^ 2) / ‖x‖ ^ 2) = x.re

Tactic:
simp [Real.sqrt_sq, (norm_pos_iff.mpr hx).le, *]

Goal state after:
case pos
x : ℂ
hx : x ≠ 0
h₁ : 0 ≤ x.re
⊢ ‖x‖ * (x.re / ‖x‖) = x.re
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
by_cases hx₁ : -1 ≤ x; swap
  · rw [not_le] at hx₁
    rw [arccos_of_le_neg_one hx₁.le, sin_pi, sqrt_eq_zero_of_nonpos]
    nlinarith
  by_cases hx₂ : x ≤ 1; swap
  · rw [not_le] at hx₂
    rw [arccos_of_one_le hx₂.le, sin_zero, sqrt_eq_zero_of_nonpos]
    nlinarith
  rw [arccos_eq_pi_div_two_sub_arcsin, sin_pi_div_two_sub, cos_arcsin]

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

Goal state before:
pp: x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
⊢ ‖x ^ (n + 1) / ↑(n + 1)!‖ ≤ ‖x‖ / (↑⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖

Tactic:
calc
    ‖x ^ (n + 1) / (n + 1)!‖ = ‖x‖ / (n + 1) * ‖x ^ n / (n !)‖ := by
      rw [_root_.pow_succ', Nat.factorial_succ, Nat.cast_mul, ← _root_.div_mul_div_comm, norm_mul,
        norm_div, Real.norm_natCast, Nat.cast_succ]
    _ ≤ ‖x‖ / (⌊‖x‖⌋₊ + 1) * ‖x ^ n / (n !)‖ := by gcongr

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

Goal state before:
pp: z : ℂ
⊢ (cexp z).arg =
    (↑(rexp z.re) * (cos ↑(toIocMod Real.two_pi_pos (-π) z.im) + sin ↑(toIocMod Real.two_pi_pos (-π) z.im) * I)).arg

Tactic:
rw [← exp_mul_I, ofReal_exp, toIocMod]
    push_cast
    rw [exp_mul_I_periodic.sub_zsmul_eq, ← exp_add, re_add_im]

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

Goal state before:
pp: case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re < 0 ∧ z.im = 0 → z.arg = π

Tactic:
· obtain ⟨x, y⟩ := z
    rintro ⟨h : x < 0, rfl : y = 0⟩
    rw [← arg_neg_one, ← arg_real_mul (-1) (neg_pos.2 h)]
    simp [← ofReal_def]

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

Goal state before:
pp: case neg.mpr
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : y < 0
⊢ { re := 0, im := y }.arg = (↑(-y) * -I).arg

Tactic:
mk_eq_add_mul_I

Goal state after:
case neg.mpr
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : y < 0
⊢ (↑0 + ↑y * I).arg = (↑(-y) * -I).arg
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ - ↑π = θ + ↑π

Tactic:
sub_eq_add_neg,

Goal state after:
θ : Angle
⊢ θ + -↑π = θ + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
hx : 0 ≤ x.im
x✝ : ∃ n, x = ↑n * (2 * ↑π * I)
n : ℕ
hn : x = ↑n * (2 * ↑π * I)
⊢ x = ↑↑n * (2 * ↑π * I)

Tactic:
by rw [hn]; norm_cast

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

Goal state before:
pp: s : Set ℂ
⊢ (cexp ⁻¹' s).Countable ↔ s.Countable

Tactic:
refine ⟨fun hs => ?_, fun hs => ?_⟩

Goal state after:
case refine_1
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
⊢ s.Countable

case refine_2
s : Set ℂ
hs : s.Countable
⊢ (cexp ⁻¹' s).Countable
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto log (𝓝[{z | z.im < 0}] z) (𝓝 (↑(Real.log ‖z‖) - ↑π * I))

Tactic:
convert!
    (continuous_ofReal.continuousAt.comp_continuousWithinAt
          (continuous_norm.continuousWithinAt.log _)).tendsto.add
      (((continuous_ofReal.tendsto _).comp <|
            tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero hre him).mul
        tendsto_const_nhds) using 1
  · simp [sub_eq_add_neg]
  · lift z to ℝ using him
    simpa using hre.ne

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

Goal state before:
pp: case refine_2
x : ℂ
h : x ∈ slitPlane
h_cont_mul : Continuous fun x ↦ x * I
⊢ ContinuousAt arg x

Tactic:
exact continuousAt_arg h

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
n : ℕ
h : NormNum.IsNat e n
w : Nat.blt 1 n = true
⊢ 1 < ↑n

Tactic:
simpa using w

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 1 < ↑n

Tactic:
simpa using w

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

Goal state before:
pp: x y z : ℂ
hx : x ≠ 0
⊢ x ^ (y - z) = x ^ y / x ^ z

Tactic:
sub_eq_add_neg,

Goal state after:
x y z : ℂ
hx : x ≠ 0
⊢ x ^ (y + -z) = x ^ y / x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
d n : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
h₁' : 0 < ↑n / ↑d
⊢ Real.log (↑n / ↑d) ≠ 0

Tactic:
have h₂' : (n : ℝ) / d < 1 := by
      simpa using (Rat.cast_lt (K := ℝ)).2 (of_decide_eq_true h₂)

Goal state after:
e : ℝ
d n : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
h₁' : 0 < ↑n / ↑d
h₂' : ↑n / ↑d < 1
⊢ Real.log (↑n / ↑d) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case hlt
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ -π / ↑n < x.arg

Tactic:
neg_div

Goal state after:
case hlt
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ -(π / ↑n) < x.arg
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ.sin = 0 ↔ θ = 0 ∨ θ = ↑π

Tactic:
← sin_zero

Goal state after:
θ : Angle
⊢ θ.sin = sin 0 ↔ θ = 0 ∨ θ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ.sin ≠ 0 ↔ ¬(θ = 0 ∨ θ = ↑π)

Tactic:
← sin_eq_zero_iff

Goal state after:
θ : Angle
⊢ θ.sin ≠ 0 ↔ ¬θ.sin = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: r : ℝ
hr : 0 < r
θ : ℝ
⊢ (↑r * (cos ↑θ + sin ↑θ * I)).arg - θ = 2 * π * ↑⌊(π - θ) / (2 * π)⌋

Tactic:
by
  rw [arg_mul_cos_add_sin_mul_I_eq_toIocMod hr, toIocMod_sub_self, toIocDiv_eq_neg_floor,
    zsmul_eq_mul]
  ring_nf

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

Goal state before:
pp: θ : Angle
⊢ θ.cos < 0 ↔ π / 2 < |θ.toReal|

Tactic:
contrapose!; exact cos_nonneg_iff_abs_toReal_le_pi_div_two

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
this : Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
⊢ (↑(rexp (log (-x) * y) * cos (y * π))).re + (↑(rexp (log (-x) * y) * sin (y * π)) * Complex.I).re =
    rexp (log x * y) * cos (y * π)

Tactic:
Complex.ofReal_re,

Goal state after:
x : ℝ
hx : x < 0
y : ℝ
this : Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
⊢ rexp (log (-x) * y) * cos (y * π) + (↑(rexp (log (-x) * y) * sin (y * π)) * Complex.I).re =
    rexp (log x * y) * cos (y * π)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case hnc
x : ℝ
hx : x < 0
y : ℝ
⊢ ¬↑x = 0

Tactic:
rw [Complex.ofReal_eq_zero]

Goal state after:
case hnc
x : ℝ
hx : x < 0
y : ℝ
⊢ ¬x = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl
x y : ℝ
hx : 0 ≤ x
⊢ |x ^ y| ≤ |x| ^ y

Tactic:
rw [abs_rpow_of_nonneg hx]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: k : ℕ
b : ℝ
hb : 0 < b
⊢ (fun x ↦ x ^ k) =o[atTop] fun x ↦ rexp (b * x)

Tactic:
simpa using isLittleO_zpow_exp_pos_mul_atTop k hb

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: z w : ℂ
⊢ ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
by_cases! h : z = 0 → w.re = 0 → w = 0
  · exact (norm_cpow_of_imp h).le
  · simp [h]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x ≠ 0
y : ℝ
⊢ x ^ (y + 1) = x ^ y * x

Tactic:
by
  simpa using rpow_add_natCast hx y 1

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
⊢ 0 < 1

Tactic:
exact one_pos

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
y : ℝ
⊢ ↑x ^ y = ↑0 ↔ x = 0 ∧ y ≠ 0

Tactic:
← NNReal.coe_eq_zero

Goal state after:
x : ℝ≥0
y : ℝ
⊢ ↑x ^ y = ↑0 ↔ ↑x = 0 ∧ y ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
hx : x ≠ 0
y : ℝ
⊢ x ^ (y + 1) = x ^ y * x

Tactic:
by
  simpa using rpow_add_natCast hx y 1

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x < y ^ z⁻¹ ↔ y < x ^ z

Tactic:
rw [← rpow_lt_rpow_iff_of_neg _ hx hz, rpow_inv_rpow _ hz.ne] <;> positivity

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
⊢ 0 < 1

Tactic:
exact one_pos

Goal state after: