mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
h : S ≤ T
⊢ ∀ (x : (M ⧸ S) ⧸ Subgroup.map (mk' S) T), ‖(quotientQuotientEquivQuotient S T h) x‖ = ‖x‖

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
h : S ≤ T
⊢ ∀ (x : (M ⧸ S) ⧸ Subgroup.map (mk' S) T), ‖(quotientQuotientEquivQuotient S T h) x‖ = ‖x‖
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ ⨅ y, dist (-m) ↑y = ⨅ a, ‖m + ↑a‖

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ ⨅ y, dist (-m) ↑y = ⨅ a, ‖m + ↑a‖
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: case inr
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, f x = 0
x : M ⧸ S
h : 0 < ‖f‖
⊢ ¬∃ m, ↑m = x ∧ ‖m‖ < ‖(lift S f.toAddMonoidHom hf) x‖ / ‖f‖

Tactic:
]

Goal state after:
case inr
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, f x = 0
x : M ⧸ S
h : 0 < ‖f‖
⊢ ¬∃ m, ↑m = x ∧ ‖m‖ < ‖(lift S f.toAddMonoidHom hf) x‖ / ‖f‖
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ closedBall x δ = closedBall x δ

Tactic:
]

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
⊢ x ∈ univ

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
⊢ x ∈ univ
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
hker : x ∈ S.topologicalClosure
⊢ ‖S.normedMk x‖ ≤ 0 * ‖x‖

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
hker : x ∈ S.topologicalClosure
⊢ ‖S.normedMk x‖ ≤ 0 * ‖x‖
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
⊢ (↑f.ker).Nonempty

Tactic:
]

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
⊢ (↑f.ker).Nonempty
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
⊢ sin (π / 2 - y) < sin (π / 2 - x)

Tactic:
]

Goal state after:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
⊢ sin (π / 2 - y) < sin (π / 2 - x)
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| ≤ a ^ n
⊢ |f n| ≤ a ^ n

Tactic:
]

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
δ : ℝ
x : E
⊢ sphere x δ = sphere x δ

Tactic:
]

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
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : ((fun m' ↦ ‖m + m'‖) '' ↑f.ker).Nonempty
x : M
hx : x ∈ ↑f.ker
H : ‖m + x‖ < sInf ((fun m' ↦ ‖m + m'‖) '' ↑f.ker) + ε
⊢ f m = f m

Tactic:
]

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

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

Tactic:
]

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ s * ball 1 δ = ⋃ x ∈ s, ball x δ
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : ((fun m' ↦ ‖m + m'‖) '' ↑f.ker).Nonempty
x : M
hx : x ∈ ↑f.ker
H : ‖m + x‖ < sInf ((fun m' ↦ ‖m + m'‖) '' ↑f.ker) + ε
⊢ ‖m + x‖ < sInf ((fun m_1 ↦ ‖m + m_1‖) '' ↑f.ker) + ε

Tactic:
]

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : ((fun m' ↦ ‖m + m'‖) '' ↑f.ker).Nonempty
x : M
hx : x ∈ ↑f.ker
H : ‖m + x‖ < sInf ((fun m' ↦ ‖m + m'‖) '' ↑f.ker) + ε
⊢ ‖m + x‖ < sInf ((fun m_1 ↦ ‖m + m_1‖) '' ↑f.ker) + ε
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
⊢ sInf ((fun m_1 ↦ ‖m + m_1‖) '' ↑f.ker) ≤ ‖m‖

Tactic:
]

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
⊢ sInf ((fun m_1 ↦ ‖m + m_1‖) '' ↑f.ker) ≤ ‖m‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ (Icc (-1) 1).Infinite

Tactic:
]

Goal state after:
⊢ (Icc (-1) 1).Infinite
Module: Mathlib.Analysis.Normed.Group.Pointwise

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: n : ℕ
⊢ sqrtTwoAddSeries 0 n < 2 ^ 2 - 2

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

Tactic:
]

Goal state after:
n : ℕ
⊢ sqrtTwoAddSeries 0 n < 2 ^ 2 - 2

n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
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 ≤ δ
⊢ s * closedBall 1 δ = ⋃ x ∈ s, closedBall x δ

Tactic:
]

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ s * closedBall 1 δ = ⋃ x ∈ s, closedBall x δ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
n : ℕ
⊢ √(2 + (√(2 + x)).sqrtTwoAddSeries n) = √(2 + (√(2 + x)).sqrtTwoAddSeries n)

Tactic:
]

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

Goal state before:
pp: x y : ℝ
h : x ≤ y
n : ℕ
⊢ √(2 + x.sqrtTwoAddSeries n) ≤ √(2 + y.sqrtTwoAddSeries n)

Tactic:
]

Goal state after:
x y : ℝ
h : x ≤ y
n : ℕ
⊢ √(2 + x.sqrtTwoAddSeries n) ≤ √(2 + y.sqrtTwoAddSeries n)
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 ≤ δ
⊢ cthickening δ s = cthickening δ s

Tactic:
]

Goal state after:
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
⊢ x • cthickening δ s = x • cthickening δ s

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
ht : 0 ≤ t
x : E
⊢ t * ‖x‖ = t * ‖x‖

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ (1 - r) * ‖x - y‖ = (1 - r) * ‖x - y‖

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ dist y x = dist y x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case e'_5
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
⊢ y = y

Tactic:
]

Goal state after:
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
⊢ ‖y - x‖ * c < r * 1

Tactic:
]

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 * 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 - 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 * 1

Tactic:
]

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 - 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 * 1
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)
⊢ √(2 + sqrtTwoAddSeries 0 n) / 2 = √(2 + sqrtTwoAddSeries 0 n) / 2

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

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

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:
]

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

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

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.Ball.Pointwise

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
this : ‖c‖₊ • ediam s ≤ ediam (c • s)
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)

Tactic:
]

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
this : ‖c‖₊ • ediam s ≤ ediam (c • s)
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)
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
⊢ sphere x r = sphere x r

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : r < 0
⊢ ∅ = ∅

Tactic:
]

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

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

Tactic:
]

Goal state after:
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

n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
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 : ℕ
⊢ ‖↑n‖ ≤ (r' - 1)⁻¹ * ‖r' ^ n‖ * ‖1‖

Tactic:
]

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 : ℕ
⊢ ‖↑n‖ ≤ (r' - 1)⁻¹ * ‖r' ^ n‖ * ‖1‖
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c ↦ c • (y - x) + x
c : ℝ
hc : c ∈ f ⁻¹' closedBall x (dist y x)
⊢ ‖c‖ * dist y x ≤ 1 * dist y x

Tactic:
]

Goal state after:
case inr.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c ↦ c • (y - x) + x
c : ℝ
hc : c ∈ f ⁻¹' closedBall x (dist y x)
⊢ ‖c‖ * dist y x ≤ 1 * dist y x
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
⊢ ∅ = ∅

Tactic:
]

Goal state after:
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

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

case hy
n : ℕ
⊢ 0 ≤ sin (π / 2 ^ (n + 2)) * 2
Module: Mathlib.Analysis.SpecificLimits.Normed

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
case hx
n : ℕ
⊢ sqrtTwoAddSeries 0 n ≤ 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
⊢ ∅ = ∅

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ sphere x r = sphere x r

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ ∅ = ∅

Tactic:
]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ c⁻¹ • y ∈ ball x r ↔ y ∈ ball (c • x) (‖c‖ * r)

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ c⁻¹ • y ∈ ball x r ↔ y ∈ ball (c • x) (‖c‖ * r)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case neg
k : ℕ
r : ℝ
hr : |r| < 1
h0 : ¬r = 0
hr' : 1 < |r|⁻¹
⊢ Tendsto (fun x ↦ ‖↑x ^ k * r ^ x‖) atTop (𝓝 0)

Tactic:
]

Goal state after:
case neg
k : ℕ
r : ℝ
hr : |r| < 1
h0 : ¬r = 0
hr' : 1 < |r|⁻¹
⊢ Tendsto (fun x ↦ ‖↑x ^ k * r ^ x‖) atTop (𝓝 0)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
⊢ ball 0 ‖c‖ = ball 0 ‖c‖

Tactic:
]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ c⁻¹ • y ∈ sphere x r ↔ y ∈ sphere (c • x) (‖c‖ * r)

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ c⁻¹ • y ∈ sphere x r ↔ y ∈ sphere (c • x) (‖c‖ * r)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
⊢ c • closedBall x r = closedBall (c • x) (‖c‖ * r)

Tactic:
by
  simp only [← ball_union_sphere, Set.smul_set_union, _root_.smul_ball hc, smul_sphere' hc]

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

Goal state before:
pp: R : Type u_2
inst✝¹ : SeminormedRing R
inst✝ : NormMulClass R
x : R
⊢ Tendsto (fun x_1 ↦ ‖x ^ x_1‖) atTop (𝓝 0) → Tendsto (fun n ↦ ‖x‖ ^ n) atTop (𝓝 0)

Tactic:
]

Goal state after:
R : Type u_2
inst✝¹ : SeminormedRing R
inst✝ : NormMulClass R
x : R
⊢ Tendsto (fun x_1 ↦ ‖x ^ x_1‖) atTop (𝓝 0) → Tendsto (fun n ↦ ‖x‖ ^ n) atTop (𝓝 0)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set 𝕜
hs : 0 ∉ s
r : ℝ
c : 𝕜
hc : c ∈ s
⊢ sphere 0 (‖c‖ * r) = sphere 0 (‖c‖ * r)

Tactic:
]

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

Goal state before:
pp: ⊢ √3 / 2 = √3 / 2

pp: ⊢ 0 ≤ 2

pp: case hx
⊢ 0 ≤ 3

pp: ⊢ 2 ≠ 0

pp: case hl
⊢ -π ≤ π / 3

pp: case hr
⊢ π / 3 ≤ π

Tactic:
]

Goal state after:
⊢ 0 ≤ 2

case hx
⊢ 0 ≤ 3

⊢ 2 ≠ 0

case hl
⊢ -π ≤ π / 3

case hr
⊢ π / 3 ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ 3 / 2 ^ 2 = 3 / 4

pp: ⊢ 0 ≤ 3

Tactic:
]

Goal state after:
⊢ 3 / 2 ^ 2 = 3 / 4

⊢ 0 ≤ 3
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 2 - π / 6) = cos (π / 3)

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: ⊢ cos (π / 2 - π / 3) = cos (π / 6)

Tactic:
]

Goal state after:
⊢ cos (π / 2 - π / 3) = cos (π / 6)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 < r
⊢ ball 0 r = ball 0 r

Tactic:
]

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

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ ¬∃ n, ↑n * π = π / 5

Tactic:
]

Goal state after:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ ¬∃ n, ↑n * π = π / 5
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
this : EqOn (fun x ↦ ‖x‖) id (Ioo a b)
⊢ (fun x ↦ ‖x‖) ⁻¹' Ioo (a * r) (b * r) = ball 0 (b * r) \ closedBall 0 (a * r)

Tactic:
]

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
this : EqOn (fun x ↦ ‖x‖) id (Ioo a b)
⊢ (fun x ↦ ‖x‖) ⁻¹' Ioo (a * r) (b * r) = ball 0 (b * r) \ closedBall 0 (a * r)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ s * 2 * c = s * 2 * c

Tactic:
]

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

Goal state before:
pp: case h
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ dist (1 • x) (a • x + b • z) = b * dist x z ∧ dist (a • x + b • z) z = a * dist x z

Tactic:
]

Goal state after:
case h
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ dist (1 • x) (a • x + b • z) = b * dist x z ∧ dist (a • x + b • z) z = a * dist x z
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case h
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ dist (1 • x) (a • x + b • z) = b * dist x z ∧ dist (a • x + b • z) (1 • z) = a * dist x z

Tactic:
]

Goal state after:
case h
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ dist (1 • x) (a • x + b • z) = b * dist x z ∧ dist (a • x + b • z) (1 • z) = a * dist x z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ 2 * s * c = 2 * sin θ * cos θ

Tactic:
]

Goal state after: