mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ cexp x * cexp (y * I) = cexp x * (cos y + sin y * I)

Tactic:
exp_mul_I

Goal state after:
x y : ℂ
⊢ cexp x * (cos y + sin y * I) = cexp x * (cos y + sin y * I)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / ↑m.factorial‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / ↑m.factorial‖ / 2 ≤
    ‖-x * I‖ ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹) / 2 +
      ‖x * I‖ ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹) / 2

Tactic:
grw [exp_bound (by simpa) (by simp), exp_bound (by simpa) (by simp)]

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

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖cexp (-x * I) - ∑ m ∈ range 5, (-x * I) ^ m / ↑m.factorial‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 5, (x * I) ^ m / ↑m.factorial‖ / 2 ≤
    ‖-x * I‖ ^ 5 * (↑(Nat.succ 5) * (↑(Nat.factorial 5) * ↑5)⁻¹) / 2 +
      ‖x * I‖ ^ 5 * (↑(Nat.succ 5) * (↑(Nat.factorial 5) * ↑5)⁻¹) / 2

Tactic:
grw [exp_bound (by simpa) (by simp), exp_bound (by simpa) (by simp)]

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

Goal state before:
pp: x : ℝ
hx : |x| ≤ 1
⊢ |cos x - (1 - x ^ 2 / 2)| ≤ |x| ^ 4 * (5 / 96)

Tactic:
simpa [← ofReal_cos, ← norm_eq_abs, ← norm_real] using Complex.cos_bound (x := x) (by simpa)

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

Goal state before:
pp: x : ℝ
⊢ ‖cexp (↑x * I)‖ = 1

Tactic:
exp_mul_I,

Goal state after:
x : ℝ
⊢ ‖cos ↑x + sin ↑x * I‖ = 1
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x)‖ = 1

Tactic:
mul_comm,

Goal state after:
x : ℝ
⊢ ‖cexp (↑x * I)‖ = 1
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = 1 * ‖1 - cexp (↑x * I)‖

Tactic:
one_mul,

Goal state after:
x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖1 - cexp (↑x * I)‖
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Field α
inst✝ : LinearOrder α
p : ℤ
hp : Even p
a : α
h : |a| = a
⊢ |a| ^ p = a ^ p

Tactic:
simp only [h, hp.neg_zpow _]

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : Field α
inst✝ : LinearOrder α
p : ℤ
hp : Even p
a : α
h : |a| = -a
⊢ |a| ^ p = a ^ p

Tactic:
simp only [h, hp.neg_zpow _]

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

Goal state before:
pp: n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ rexp (-(↑n * (t / ↑n))) = rexp (-t)

Tactic:
mul_comm,

Goal state after:
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ rexp (-(t / ↑n * ↑n)) = rexp (-t)
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: n : ℕ
x : ℝ
⊢ 1 * x ^ n / rexp x = x ^ n * rexp (-x)

Tactic:
one_mul,

Goal state after:
n : ℕ
x : ℝ
⊢ x ^ n / rexp x = x ^ n * rexp (-x)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
h : cos x = 1
n : ℤ
hn : 1 * π + ↑(2 * (n / 2)) * π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x

Tactic:
one_mul,

Goal state after:
x : ℝ
h : cos x = 1
n : ℤ
hn : π + ↑(2 * (n / 2)) * π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
m : M
⊢ ‖↑m‖ = 0 ↔ m ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S

Tactic:
by
  rw [norm_mk, ← mem_closure_iff_infDist_zero]
  exact ⟨1, S.one_mem⟩

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ ball x δ * {y} = ball (x * y) δ

Tactic:
mul_comm,

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ {y} * ball x δ = ball (x * y) δ
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 : (∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_2_to_1 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x
tfae_3_to_2 : (∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x
tfae_2_to_4 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_3 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_6 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n) →
    ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_5_to_3 :
  (∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
a : ℝ
ha : a ∈ Set.Ioo 0 R
H : f =o[atTop] fun x ↦ a ^ x
n : ℕ
hn : |f n| ≤ 1 * |a ^ n|
⊢ |f n| ≤ a ^ n

Tactic:
one_mul,

Goal state after:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 : (∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_2_to_1 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x
tfae_3_to_2 : (∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x
tfae_2_to_4 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_3 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_6 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n) →
    ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_5_to_3 :
  (∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
a : ℝ
ha : a ∈ Set.Ioo 0 R
H : f =o[atTop] fun x ↦ a ^ x
n : ℕ
hn : |f n| ≤ |a ^ n|
⊢ |f n| ≤ a ^ n
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ ball 1 δ * s = thickening δ s

Tactic:
mul_comm,

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ s * ball 1 δ = thickening δ s
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
x : E
⊢ ball x δ * s = x • thickening δ s

Tactic:
mul_comm,

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
x : E
⊢ s * ball x δ = x • thickening δ s
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ closedBall 1 δ * s = cthickening δ s

Tactic:
mul_comm,

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ s * closedBall 1 δ = cthickening δ s
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ closedBall x δ * s = x • cthickening δ s

Tactic:
mul_comm,

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ s * closedBall x δ = x • cthickening δ s
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✝ : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < ‖(mk I) a‖ + ε₁
b : R
h :
  ∀ (a_1 b_1 : ℝ), dist a_1 ‖(mk I) a‖ < ε₁ → dist b_1 ‖(mk I) b‖ < ε₂ → dist (a_1 * b_1) (‖(mk I) a‖ * ‖(mk I) b‖) < ε
hb : ‖b‖ < ‖(mk I) b‖ + ε₂
⊢ ‖(mk I) a * (mk I) b‖ ≤ ‖(mk I) a‖ * ‖(mk I) b‖ + ε

Tactic:
simp only [dist, abs_sub_lt_iff] at h

Goal state after:
M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < ‖(mk I) a‖ + ε₁
b : R
hb : ‖b‖ < ‖(mk I) b‖ + ε₂
h :
  ∀ (a_1 b_1 : ℝ),
    a_1 - ‖(mk I) a‖ < ε₁ ∧ ‖(mk I) a‖ - a_1 < ε₁ →
      b_1 - ‖(mk I) b‖ < ε₂ ∧ ‖(mk I) b‖ - b_1 < ε₂ →
        a_1 * b_1 - ‖(mk I) a‖ * ‖(mk I) b‖ < ε ∧ ‖(mk I) a‖ * ‖(mk I) b‖ - a_1 * b_1 < ε
⊢ ‖(mk I) a * (mk I) b‖ ≤ ‖(mk I) a‖ * ‖(mk I) b‖ + ε
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 * 2 + sqrtTwoAddSeries 0 n) / 2 / 2) = √(2 + sqrtTwoAddSeries 0 n) / 2

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

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:
one_mul,

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

case hc
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ 2 ≠ 0

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.Normed.Module.RCLike.Real

Goal state before:
pp: case convert_3
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt (fun c ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
⊢ c * ‖y - x‖ < r

Tactic:
mul_comm,

Goal state after:
case convert_3
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt (fun c ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
⊢ ‖y - x‖ * c < r
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
| r' ^ (k * n)

Tactic:
mul_comm,

Goal state after:
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
| r' ^ (n * k)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective fun x ↦ c • x
⊢ ⨅ y ∈ c • s, edist (c • x) y = ‖c‖₊ • ⨅ y ∈ s, edist x y

Tactic:
trans ⨅ (y) (_ : y ∈ s), ‖c‖₊ • edist x y

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective fun x ↦ c • x
⊢ ⨅ y ∈ c • s, edist (c • x) y = ⨅ y ∈ s, ‖c‖₊ • edist x y

𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective fun x ↦ c • x
⊢ ⨅ y ∈ s, ‖c‖₊ • edist x y = ‖c‖₊ • ⨅ y ∈ s, edist x y
Module: Mathlib.Analysis.SpecificLimits.Normed

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

Tactic:
simpa [div_mul_cancel₀ _ (pow_pos h0 _).ne', div_pow] using A.mul_isBigO this

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁵ : Field R
inst✝⁴ : Field S
inst✝³ : LinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : 1 < v a
⊢ Tendsto (fun n ↦ v (1 * (1 + a ^ n)⁻¹)) atTop (𝓝 0)

Tactic:
one_mul,

Goal state after:
R : Type u_2
S : Type u_3
inst✝⁵ : Field R
inst✝⁴ : Field S
inst✝³ : LinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : 1 < v a
⊢ Tendsto (fun n ↦ v (1 + a ^ n)⁻¹) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ tan (π / 2) = 0

Tactic:
simp [tan_eq_sin_div_cos]

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

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ 1 * ∑' (i : ℕ), x ^ i + x * ∑' (i : ℕ), x ^ i = 2 * ∑' (i : ℕ), x ^ i - 1

Tactic:
one_mul,

Goal state after:
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ ∑' (i : ℕ), x ^ i + x * ∑' (i : ℕ), x ^ i = 2 * ∑' (i : ℕ), x ^ i - 1
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: K : Type u_4
inst✝ : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun n ↦ (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹))
⊢ HasSum (fun n ↦ ξ ^ n) (1 - ξ)⁻¹

Tactic:
rw [hasSum_iff_tendsto_nat_of_summable_norm]

Goal state after:
K : Type u_4
inst✝ : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun n ↦ (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹))
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, ξ ^ i) atTop (𝓝 (1 - ξ)⁻¹)

K : Type u_4
inst✝ : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun n ↦ (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹))
⊢ Summable fun i ↦ ‖ξ ^ i‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
hlt : x < y
⊢ sin x * cos y < sin y * cos x

Tactic:
mul_comm,

Goal state after:
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
hlt : x < y
⊢ cos y * sin x < sin y * cos x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ 0 + 1 * I = I

Tactic:
one_mul,

Goal state after:
⊢ 0 + I = I
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:
neg_ball,

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.closedBall a ε + -Metric.ball b δ = Metric.ball (a + -b) (ε + δ)

Tactic:
neg_ball,

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.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
⊢ (𝓝 f).HasBasis
    (fun S ↦ S.Finite ∧ ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K ∧ IsOpen[inst✝] U ∧ MapsTo (⇑f) K U) fun x ↦
    ⋂ KU ∈ x, {g | MapsTo (⇑g) KU.1 KU.2}

Tactic:
refine ⟨fun s ↦ ?_⟩
  simp_rw [nhds_compactOpen, iInf_comm.{_, 0, _ + 1}, iInf_prod', iInf_and']
  simp [mem_biInf_principal, and_assoc]

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

Goal state before:
pp: α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f (b + 1)‖ ≤ r * ‖f b‖
n : ℕ
| ‖f N‖ * r ^ n

Tactic:
mul_comm,

Goal state after:
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f (b + 1)‖ ≤ r * ‖f b‖
n : ℕ
| r ^ n * ‖f N‖
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, connectedComponent x = univ

Tactic:
rcases isPathConnected_iff_eq.mp (pathConnectedSpace_iff_univ.mp ‹_›) with ⟨x, _x_in, hx⟩

Goal state after:
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
⊢ ∃ x, connectedComponent x = univ
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case h
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
⊢ univ ⊆ connectedComponent x

Tactic:
exact (by simpa using hx : pathComponent x = univ) ▸ pathComponent_subset_component x

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
γ : Path x y
f : X → Y
h : Continuous[inst✝¹, inst✝] f
⊢ ⇑(γ.map h) = f ∘ ⇑γ

Tactic:
by
  ext t
  rfl

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 ↦ ∑ i ∈ Finset.range n, f i • z i

Tactic:
← cauchySeq_shift 1

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 ↦ ∑ i ∈ Finset.range (n + 1), f i • z i
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr
p : ℝ
hp : p ≠ 0
⊢ |p / 2 - 1 * p| = |p| / 2

Tactic:
one_mul,

Goal state after:
case inr
p : ℝ
hp : p ≠ 0
⊢ |p / 2 - p| = |p| / 2
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + 1 * f (2 * n) + -f (2 * n + 1) ≤
    ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x

Tactic:
one_mul,

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + f (2 * n) + -f (2 * n + 1) ≤ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
⊢ γ.truncate 0 0 = (refl a).cast ⋯ ⋯

Tactic:
by
  convert! γ.truncate_self 0

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

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i ≤
    ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i + -f (2 * n + 1) + 1 * f (2 * n + 1 + 1)

Tactic:
one_mul,

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i ≤
    ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i + -f (2 * n + 1) + f (2 * n + 1 + 1)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤
    ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + 1 * f (2 * n) + -f (2 * n + 1)

Tactic:
one_mul,

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + f (2 * n) + -f (2 * n + 1)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + -f (2 * n + 1) + 1 * f (2 * n + 2) ≤
    ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x

Tactic:
one_mul,

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + -f (2 * n + 1) + f (2 * n + 2) ≤
    ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case pos
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ ∈ Icc (-(π / 2)) (π / 2)
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Tactic:
if_pos

Goal state after:
case pos
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ ∈ Icc (-(π / 2)) (π / 2)
⊢ Real.arcsin (Real.sin θ) = θ

case pos.hc
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ ∈ Icc (-(π / 2)) (π / 2)
⊢ 0 ≤ Real.cos θ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.inl
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Tactic:
have hsin : Real.sin θ < 0 := Real.sin_neg_of_neg_of_neg_pi_lt (by linarith) hθ

Goal state after:
case neg.inl
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x y : ℝ
h : 0 < x
h₁ : 0 < y
⊢ rexp (log x) ≤ rexp (log y) ↔ x ≤ y

Tactic:
exp_log h,

Goal state after:
x y : ℝ
h : 0 < x
h₁ : 0 < y
⊢ x ≤ rexp (log y) ↔ x ≤ y
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case inl
x y : ℝ
h : log x < y
hx : x ≤ 0
⊢ x < rexp y

Tactic:
exact hx.trans_lt <| exp_pos y

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

Goal state before:
pp: n : ℤ
x✝ : 0 < n ∨ 0 = n ∨ n < 0
⊢ 0 ≤ log ↑n

Tactic:
cases lt_trichotomy 0 n with

Goal state after: