mathlib-initiative/mathlib-tactics huggingface dataset:
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 = ⨅ y ∈ s, ‖c‖₊ • edist x y

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 ∈ s, ‖c‖₊ • edist x y = ‖c‖₊ • ⨅ y ∈ s, edist x y

Tactic:
·

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
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℕ
⊢ 1 - 2 / 2 ^ 2 - sqrtTwoAddSeries 0 n / 2 ^ 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4

pp: n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n

Tactic:
·

Goal state after:
n : ℕ
⊢ 1 - 2 / 2 ^ 2 - sqrtTwoAddSeries 0 n / 2 ^ 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case e_a
n : ℕ
⊢ 1 - 2 / 2 ^ 2 = 1 / 2

pp: case e_a.e_a
n : ℕ
⊢ 2 ^ 2 = 4

Tactic:
·

Goal state after:
case e_a
n : ℕ
⊢ 1 - 2 / 2 ^ 2 = 1 / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case e_a.e_a
n : ℕ
⊢ 2 ^ 2 = 4

Tactic:
·

Goal state after:
case e_a.e_a
n : ℕ
⊢ 2 ^ 2 = 4
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℕ
⊢ sin (π / 2 ^ (n + 2)) ^ 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4

Tactic:
rw [sin_sq_pi_over_two_pow, sqrtTwoAddSeries, div_pow, sq_sqrt, add_div, ← sub_sub]
  · congr
    · norm_num
    · norm_num
  · exact add_nonneg two_pos.le (sqrtTwoAddSeries_zero_nonneg _)

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

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

pp: case neg
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : ¬r₁ = 0
⊢ (fun n ↦ ↑n ^ k * r₁ ^ n) =o[atTop] fun n ↦ r₂ ^ n

Tactic:
·

Goal state after:
case pos
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : r₁ = 0
⊢ (fun n ↦ ↑n ^ k * r₁ ^ n) =o[atTop] fun n ↦ r₂ ^ n
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (sphere x r) = ∅

Tactic:
← frontier_closedBall x hr,

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (frontier (closedBall x r)) = ∅
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 ∈ s, ‖c‖₊ • edist x y = ‖c‖₊ • ⨅ y ∈ s, edist x y

Tactic:
·

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 ∈ s, ‖c‖₊ • edist x y = ‖c‖₊ • ⨅ y ∈ s, edist x y
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℕ
⊢ 2 - sqrtTwoAddSeries 0 n = 1 / 2 * 2 ^ 2 - sqrtTwoAddSeries 0 n / 4 * 2 ^ 2

pp: case hx
n : ℕ
⊢ 0 ≤ 2 - sqrtTwoAddSeries 0 n

pp: case hy
n : ℕ
⊢ 0 ≤ sin (π / 2 ^ (n + 2)) * 2

Tactic:
·

Goal state after:
n : ℕ
⊢ 2 - sqrtTwoAddSeries 0 n = 1 / 2 * 2 ^ 2 - sqrtTwoAddSeries 0 n / 4 * 2 ^ 2
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
⊢ interior (closedBall x 0) = ball x 0

pp: case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (closedBall x r) = ball x r

Tactic:
·

Goal state after:
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
⊢ interior (closedBall x 0) = ball x 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case hx
n : ℕ
⊢ 0 ≤ 2 - sqrtTwoAddSeries 0 n

pp: case hy
n : ℕ
⊢ 0 ≤ sin (π / 2 ^ (n + 2)) * 2

Tactic:
·

Goal state after:
case hx
n : ℕ
⊢ 0 ≤ 2 - sqrtTwoAddSeries 0 n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case hy.refine_1
n : ℕ
⊢ 0 ≤ π / 2 ^ (n + 2)

pp: case hy.refine_2
n : ℕ
⊢ π / 2 ^ (n + 2) ≤ π

Tactic:
·

Goal state after:
case hy.refine_1
n : ℕ
⊢ 0 ≤ π / 2 ^ (n + 2)
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (closedBall x r) = ball x r

Tactic:
·

Goal state after:
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (closedBall x r) = ball x r
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case hy.refine_2
n : ℕ
⊢ π / 2 ^ (n + 2) ≤ π

Tactic:
·

Goal state after:
case hy.refine_2
n : ℕ
⊢ π / 2 ^ (n + 2) ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 4) = cos (π / 2 ^ 2)

pp: ⊢ cos (π / 2 ^ 2) = √2 / 2

Tactic:
·

Goal state after:
⊢ cos (π / 4) = cos (π / 2 ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 2 ^ 2) = √2 / 2

Tactic:
·

Goal state after:
⊢ cos (π / 2 ^ 2) = √2 / 2
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case pos
k : ℕ
r : ℝ
hr : |r| < 1
h0 : r = 0
⊢ Tendsto (fun n ↦ ↑n ^ k * r ^ n) atTop (𝓝 0)

pp: case neg
k : ℕ
r : ℝ
hr : |r| < 1
h0 : ¬r = 0
⊢ Tendsto (fun n ↦ ↑n ^ k * r ^ n) atTop (𝓝 0)

Tactic:
·

Goal state after:
case pos
k : ℕ
r : ℝ
hr : |r| < 1
h0 : r = 0
⊢ Tendsto (fun n ↦ ↑n ^ k * r ^ n) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 4) = sin (π / 2 ^ 2)

pp: ⊢ sin (π / 2 ^ 2) = √2 / 2

Tactic:
·

Goal state after:
⊢ sin (π / 4) = sin (π / 2 ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 2 ^ 2) = √2 / 2

Tactic:
·

Goal state after:
⊢ sin (π / 2 ^ 2) = √2 / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 8) = cos (π / 2 ^ 3)

pp: ⊢ cos (π / 2 ^ 3) = √(2 + √2) / 2

Tactic:
·

Goal state after:
⊢ cos (π / 8) = cos (π / 2 ^ 3)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 2 ^ 3) = √(2 + √2) / 2

Tactic:
·

Goal state after:
⊢ cos (π / 2 ^ 3) = √(2 + √2) / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 8) = sin (π / 2 ^ 3)

pp: ⊢ sin (π / 2 ^ 3) = √(2 - √2) / 2

Tactic:
·

Goal state after:
⊢ sin (π / 8) = sin (π / 2 ^ 3)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 2 ^ 3) = √(2 - √2) / 2

Tactic:
·

Goal state after:
⊢ sin (π / 2 ^ 3) = √(2 - √2) / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 16) = cos (π / 2 ^ 4)

pp: ⊢ cos (π / 2 ^ 4) = √(2 + √(2 + √2)) / 2

Tactic:
·

Goal state after:
⊢ cos (π / 16) = cos (π / 2 ^ 4)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 2 ^ 4) = √(2 + √(2 + √2)) / 2

Tactic:
·

Goal state after:
⊢ cos (π / 2 ^ 4) = √(2 + √(2 + √2)) / 2
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: r : ℝ
k : ℕ
hk : k ≠ 0
⊢ Tendsto (fun n ↦ r / ↑n ^ k) atTop (𝓝 0)

Tactic:
by
  simpa using Filter.Tendsto.const_div_atTop (tendsto_natCast_atTop_atTop (R := ℝ).comp
    (tendsto_pow_atTop hk)) r

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

Goal state before:
pp: ⊢ sin (π / 16) = sin (π / 2 ^ 4)

pp: ⊢ sin (π / 2 ^ 4) = √(2 - √(2 + √2)) / 2

Tactic:
·

Goal state after:
⊢ sin (π / 16) = sin (π / 2 ^ 4)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 2 ^ 4) = √(2 - √(2 + √2)) / 2

Tactic:
·

Goal state after:
⊢ sin (π / 2 ^ 4) = √(2 - √(2 + √2)) / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 32) = cos (π / 2 ^ 5)

pp: ⊢ cos (π / 2 ^ 5) = √(2 + √(2 + √(2 + √2))) / 2

Tactic:
·

Goal state after:
⊢ cos (π / 32) = cos (π / 2 ^ 5)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 2 ^ 5) = √(2 + √(2 + √(2 + √2))) / 2

Tactic:
·

Goal state after:
⊢ cos (π / 2 ^ 5) = √(2 + √(2 + √(2 + √2))) / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 32) = sin (π / 2 ^ 5)

pp: ⊢ sin (π / 2 ^ 5) = √(2 - √(2 + √(2 + √2))) / 2

Tactic:
·

Goal state after:
⊢ sin (π / 32) = sin (π / 2 ^ 5)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 2 ^ 5) = √(2 - √(2 + √(2 + √2))) / 2

Tactic:
·

Goal state after:
⊢ sin (π / 2 ^ 5) = √(2 - √(2 + √(2 + √2))) / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case inl
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : (2 * cos (π / 3) - 1) ^ 2 = 0
⊢ cos (π / 3) = 1 / 2

pp: case inr
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
⊢ cos (π / 3) = 1 / 2

Tactic:
·

Goal state after:
case inl
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : (2 * cos (π / 3) - 1) ^ 2 = 0
⊢ cos (π / 3) = 1 / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case inr
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
⊢ cos (π / 3) = 1 / 2

Tactic:
·

Goal state after:
case inr
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
⊢ cos (π / 3) = 1 / 2
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 : v a < 1
⊢ Tendsto (fun n ↦ v (1 / (1 + a ^ n))) atTop (𝓝 1)

Tactic:
simp_rw [map_div₀ v, v.map_one]
  apply one_div_one (G := S) ▸ Tendsto.div tendsto_const_nhds _ one_ne_zero
  have h_add := (tendsto_pow_atTop_nhds_zero_of_lt_one (v.nonneg _) ha).const_add 1
  have h_sub := (tendsto_pow_atTop_nhds_zero_of_lt_one (v.nonneg _) ha).const_sub 1
  exact tendsto_of_tendsto_of_tendsto_of_le_of_le (by simpa using h_sub) (by simpa using h_add)
    (fun n ↦ le_trans (by simp) (v.le_add _ _))
    (fun n ↦ le_trans (v.add_le _ _) (by simp))

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

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ 0
h : dist x z ≤ 0 + δ
⊢ ∃ y, dist x y ≤ δ ∧ dist y z ≤ 0

pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
hε' : 0 < ε
⊢ ∃ y, dist x y ≤ δ ∧ dist y z ≤ ε

Tactic:
·

Goal state after:
case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ 0
h : dist x z ≤ 0 + δ
⊢ ∃ y, dist x y ≤ δ ∧ dist y z ≤ 0
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
⊢ ‖∑' (n : ℕ), x ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

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

Tactic:
·

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

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

Tactic:
·

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

Goal state before:
pp: case inl
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / (2 * 4)
⊢ c = (1 + √5) / 4

pp: case inr
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ c = (1 + √5) / 4

Tactic:
·

Goal state after:
case inl
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / (2 * 4)
⊢ c = (1 + √5) / 4
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case inr
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ c = (1 + √5) / 4

Tactic:
·

Goal state after:
case inr
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ c = (1 + √5) / 4
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)⁻¹))
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, ξ ^ i) atTop (𝓝 (1 - ξ)⁻¹)

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)⁻¹))
⊢ Summable fun i ↦ ‖ξ ^ i‖

Tactic:
·

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 - ξ)⁻¹)
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)⁻¹))
⊢ Summable fun i ↦ ‖ξ ^ i‖

Tactic:
·

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)⁻¹))
⊢ Summable fun i ↦ ‖ξ ^ i‖
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: K : Type u_4
inst✝ : NormedDivisionRing K
ξ : K
h : Summable fun n ↦ ξ ^ n
k : ℕ
hk : ‖ξ‖ ^ k < 1
⊢ ‖ξ‖ < 1

Tactic:
rw [← one_pow k] at hk

Goal state after:
K : Type u_4
inst✝ : NormedDivisionRing K
ξ : K
h : Summable fun n ↦ ξ ^ n
k : ℕ
hk : ‖ξ‖ ^ k < 1 ^ k
⊢ ‖ξ‖ < 1
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : infEDist x s < ENNReal.ofReal δ
⊢ infEDist x (thickening δ s) = infEDist x s - ENNReal.ofReal δ

pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
⊢ infEDist x (thickening δ s) = infEDist x s - ENNReal.ofReal δ

Tactic:
·

Goal state after:
case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : infEDist x s < ENNReal.ofReal δ
⊢ infEDist x (thickening δ s) = infEDist x s - ENNReal.ofReal δ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case h1
⊢ Tendsto cos (𝓝[<] (π / 2)) (𝓝 0)

pp: case h2
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] (π / 2), cos x ∈ Ioi 0

Tactic:
·

Goal state after:
case h1
⊢ Tendsto cos (𝓝[<] (π / 2)) (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case h2
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] (π / 2), cos x ∈ Ioi 0

Tactic:
·

Goal state after:
case h2
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] (π / 2), cos x ∈ Ioi 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case h1
⊢ Tendsto cos (𝓝[>] (-(π / 2))) (𝓝 0)

pp: case h2
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] (-(π / 2)), cos x ∈ Ioi 0

Tactic:
·

Goal state after:
case h1
⊢ Tendsto cos (𝓝[>] (-(π / 2))) (𝓝 0)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n ↦ ↑((n + k).choose k) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
n : ℕ
hn : k < n
⊢ n + k ≤ 2 * n

Tactic:
by lia

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

Goal state before:
pp: case h2
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] (-(π / 2)), cos x ∈ Ioi 0

Tactic:
·

Goal state after:
case h2
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] (-(π / 2)), cos x ∈ Ioi 0
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
⊢ infEDist x (thickening δ s) = infEDist x s - ENNReal.ofReal δ

Tactic:
obtain hs | hs := lt_or_ge (infEDist x s) (ENNReal.ofReal δ)
  · rw [infEDist_zero_of_mem, tsub_eq_zero_of_le hs.le]
    exact hs
  refine (tsub_le_iff_right.2 infEDist_le_infEDist_thickening_add).antisymm' ?_
  refine le_sub_of_add_le_right ofReal_ne_top ?_
  refine le_infEDist.2 fun z hz => le_of_forall_gt fun r h => ?_
  cases r with
  | top =>
    exact add_lt_top.2 ⟨lt_top_iff_ne_top.2 <| infEDist_ne_top ⟨z, self_subset_thickening hδ _ hz⟩,
      ofReal_lt_top⟩
  | coe r =>
    have hr : 0 < ↑r - δ := by
      refine sub_pos_of_lt ?_
      have := hs.trans_lt ((infEDist_le_edist_of_mem hz).trans_lt h)
      rw [ofReal_eq_coe_nnreal hδ.le] at this
      exact mod_cast this
    rw [edist_lt_coe, ← dist_lt_coe, ← add_sub_cancel δ ↑r] at h
    obtain ⟨y, hxy, hyz⟩ := exists_dist_lt_lt hr hδ h
    refine (ENNReal.add_lt_add_right ofReal_ne_top <|
      infEDist_lt_iff.2 ⟨_, mem_thickening_iff.2 ⟨_, hz, hyz⟩, edist_lt_ofReal.2 hxy⟩).trans_le ?_
    rw [← ofReal_add hr.le hδ.le, sub_add_cancel, ofReal_coe_nnreal]

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

Goal state before:
pp: case e'_5
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n ↦ ↑((n + k).choose k) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
I1 : Summable fun n ↦ ‖↑((n + k).choose k) * r ^ n‖
n : ℕ
⊢ ↑((n + (k + 1)).choose (k + 1)) * r ^ n =
    ∑ k_1 ∈ Finset.range (n + 1), ↑((k_1 + k).choose k) * r ^ k_1 * r ^ (n - k_1)

pp: case e'_6
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n ↦ ↑((n + k).choose k) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
I1 : Summable fun n ↦ ‖↑((n + k).choose k) * r ^ n‖
⊢ (1 - r)⁻¹ʳ ^ (k + 1 + 1) = (∑' (n : ℕ), ↑((n + k).choose k) * r ^ n) * ∑' (n : ℕ), r ^ n

Tactic:
·

Goal state after:
case e'_5
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n ↦ ↑((n + k).choose k) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
I1 : Summable fun n ↦ ‖↑((n + k).choose k) * r ^ n‖
n : ℕ
⊢ ↑((n + (k + 1)).choose (k + 1)) * r ^ n =
    ∑ k_1 ∈ Finset.range (n + 1), ↑((k_1 + k).choose k) * r ^ k_1 * r ^ (n - k_1)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : δ ≤ 0
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ

pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : 0 < δ
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ

Tactic:
·

Goal state after:
case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : δ ≤ 0
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : 0 < δ
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ

Tactic:
·

Goal state after:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : 0 < δ
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
ε : ℝ
hε : 0 < ε
s : Set E
hδ : 0 ≤ 0
⊢ thickening ε (cthickening 0 s) = thickening (ε + 0) s

pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ✝ : 0 ≤ δ
s : Set E
hδ : 0 < δ
⊢ thickening ε (cthickening δ s) = thickening (ε + δ) s

Tactic:
·

Goal state after:
case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
ε : ℝ
hε : 0 < ε
s : Set E
hδ : 0 ≤ 0
⊢ thickening ε (cthickening 0 s) = thickening (ε + 0) s
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ✝ : 0 ≤ δ
s : Set E
hδ : 0 < δ
⊢ thickening ε (cthickening δ s) = thickening (ε + δ) s

Tactic:
·

Goal state after:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ✝ : 0 ≤ δ
s : Set E
hδ : 0 < δ
⊢ thickening ε (cthickening δ s) = thickening (ε + δ) s
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case e'_6
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n ↦ ↑((n + k).choose k) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
I1 : Summable fun n ↦ ‖↑((n + k).choose k) * r ^ n‖
⊢ (1 - r)⁻¹ʳ ^ (k + 1 + 1) = (∑' (n : ℕ), ↑((n + k).choose k) * r ^ n) * ∑' (n : ℕ), r ^ n

Tactic:
·

Goal state after:
case e'_6
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n ↦ ↑((n + k).choose k) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
I1 : Summable fun n ↦ ‖↑((n + k).choose k) * r ^ n‖
⊢ (1 - r)⁻¹ʳ ^ (k + 1 + 1) = (∑' (n : ℕ), ↑((n + k).choose k) * r ^ n) * ∑' (n : ℕ), r ^ n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case refine_1
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
⊢ Real.cos b ≤ Real.cos |z.im|

pp: case refine_2
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
⊢ 0 ≤ Real.cos b

Tactic:
·

Goal state after:
case refine_1
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
⊢ Real.cos b ≤ Real.cos |z.im|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case refine_2
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
⊢ 0 ≤ Real.cos b

Tactic:
·

Goal state after:
case refine_2
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
⊢ 0 ≤ Real.cos 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:
closedBall_add_closedBall hε hδ,

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