mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
r : ℝ
hr : 0 ≤ r
⊢ 0 • closedBall x r = closedBall (0 • x) (‖0‖ * r)

pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
hc : c ≠ 0
⊢ c • closedBall x r = closedBall (c • x) (‖c‖ * r)

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
r : ℝ
hr : 0 ≤ r
⊢ 0 • closedBall x r = closedBall (0 • x) (‖0‖ * r)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

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

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
hc : c ≠ 0
⊢ c • closedBall x r = closedBall (c • x) (‖c‖ * r)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
⊢ 0 • sphere x r = sphere (0 • x) (‖0‖ * r)

pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
hc : c ≠ 0
⊢ c • sphere x r = sphere (c • x) (‖c‖ * r)

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
⊢ 0 • sphere x r = sphere (0 • x) (‖0‖ * r)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
hc : c ≠ 0
⊢ c • sphere x r = sphere (c • x) (‖c‖ * r)

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
hc : c ≠ 0
⊢ c • sphere x r = sphere (c • x) (‖c‖ * r)
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case refine_1
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : s ∈ 𝓝 (const X c)
⊢ ∃ i, (IsCompact i.1 ∧ p i.2) ∧ {f | MapsTo (⇑f) i.1 (U i.2)} ⊆ s

pp: case refine_2
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : ∃ i, (IsCompact i.1 ∧ p i.2) ∧ {f | MapsTo (⇑f) i.1 (U i.2)} ⊆ s
⊢ s ∈ 𝓝 (const X c)

Tactic:
·

Goal state after:
case refine_1
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : s ∈ 𝓝 (const X c)
⊢ ∃ i, (IsCompact i.1 ∧ p i.2) ∧ {f | MapsTo (⇑f) i.1 (U i.2)} ⊆ s
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case e'_5
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n ↦ (↑n + 1) * x ^ n) ((1 - x)⁻¹ʳ ^ 2)
B : HasSum (fun n ↦ x ^ n) (1 - x)⁻¹ʳ
⊢ (fun n ↦ ↑n * x ^ n) = fun b ↦ (↑b + 1) * x ^ b - x ^ b

pp: case e'_6
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n ↦ (↑n + 1) * x ^ n) ((1 - x)⁻¹ʳ ^ 2)
B : HasSum (fun n ↦ x ^ n) (1 - x)⁻¹ʳ
⊢ x * (1 - x)⁻¹ʳ ^ 2 = (1 - x)⁻¹ʳ ^ 2 - (1 - x)⁻¹ʳ

Tactic:
·

Goal state after:
case e'_5
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n ↦ (↑n + 1) * x ^ n) ((1 - x)⁻¹ʳ ^ 2)
B : HasSum (fun n ↦ x ^ n) (1 - x)⁻¹ʳ
⊢ (fun n ↦ ↑n * x ^ n) = fun b ↦ (↑b + 1) * x ^ b - x ^ b
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case e'_6
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n ↦ (↑n + 1) * x ^ n) ((1 - x)⁻¹ʳ ^ 2)
B : HasSum (fun n ↦ x ^ n) (1 - x)⁻¹ʳ
⊢ x * (1 - x)⁻¹ʳ ^ 2 = (1 - x)⁻¹ʳ ^ 2 - (1 - x)⁻¹ʳ

Tactic:
·

Goal state after:
case e'_6
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n ↦ (↑n + 1) * x ^ n) ((1 - x)⁻¹ʳ ^ 2)
B : HasSum (fun n ↦ x ^ n) (1 - x)⁻¹ʳ
⊢ x * (1 - x)⁻¹ʳ ^ 2 = (1 - x)⁻¹ʳ ^ 2 - (1 - x)⁻¹ʳ
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
n : ℕ
⊢ ‖∑ x ∈ Finset.range n, f x + f n - ∑ i ∈ Finset.range n, f i‖ ≤ C * r ^ n

Tactic:
add_sub_cancel_left

Goal state after:
α : Type u_1
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
n : ℕ
⊢ ‖f n‖ ≤ C * r ^ n
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case refine_1.inl
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : s ∈ 𝓝 (const X c)
S : Set (Set X × Set Y)
hSf : S.Finite
hSsub : {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst✝] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c)) K U
this : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c
i : ι
hpi : p i
hi : U i ⊆ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2
f : C(X, Y)
hf : f ∈ {f | MapsTo ⇑f (⋃ KU ∈ S, KU.1, i).1 (U (⋃ KU ∈ S, KU.1, i).2)}
V : Set Y
hKV : (∅, V) ∈ S
⊢ MapsTo ⇑f ∅ V

pp: case refine_1.inr
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : s ∈ 𝓝 (const X c)
S : Set (Set X × Set Y)
hSf : S.Finite
hSsub : {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst✝] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c)) K U
this : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c
i : ι
hpi : p i
hi : U i ⊆ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2
f : C(X, Y)
hf : f ∈ {f | MapsTo ⇑f (⋃ KU ∈ S, KU.1, i).1 (U (⋃ KU ∈ S, KU.1, i).2)}
K : Set X
V : Set Y
hKV : (K, V) ∈ S
hKne : K.Nonempty
⊢ MapsTo (⇑f) K V

Tactic:
·

Goal state after:
case refine_1.inl
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : s ∈ 𝓝 (const X c)
S : Set (Set X × Set Y)
hSf : S.Finite
hSsub : {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst✝] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c)) K U
this : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c
i : ι
hpi : p i
hi : U i ⊆ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2
f : C(X, Y)
hf : f ∈ {f | MapsTo ⇑f (⋃ KU ∈ S, KU.1, i).1 (U (⋃ KU ∈ S, KU.1, i).2)}
V : Set Y
hKV : (∅, V) ∈ S
⊢ MapsTo ⇑f ∅ V
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case refine_1.inr
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : s ∈ 𝓝 (const X c)
S : Set (Set X × Set Y)
hSf : S.Finite
hSsub : {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst✝] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c)) K U
this : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c
i : ι
hpi : p i
hi : U i ⊆ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2
f : C(X, Y)
hf : f ∈ {f | MapsTo ⇑f (⋃ KU ∈ S, KU.1, i).1 (U (⋃ KU ∈ S, KU.1, i).2)}
K : Set X
V : Set Y
hKV : (K, V) ∈ S
hKne : K.Nonempty
⊢ MapsTo (⇑f) K V

Tactic:
·

Goal state after:
case refine_1.inr
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : s ∈ 𝓝 (const X c)
S : Set (Set X × Set Y)
hSf : S.Finite
hSsub : {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst✝] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c)) K U
this : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c
i : ι
hpi : p i
hi : U i ⊆ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2
f : C(X, Y)
hf : f ∈ {f | MapsTo ⇑f (⋃ KU ∈ S, KU.1, i).1 (U (⋃ KU ∈ S, KU.1, i).2)}
K : Set X
V : Set Y
hKV : (K, V) ∈ S
hKne : K.Nonempty
⊢ MapsTo (⇑f) K V
Module: Mathlib.Analysis.SpecificLimits.Normed

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

pp: α : Type u_1
inst✝ : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
v : ℕ → α := ⋯
hC : 0 ≤ C
this : ∀ n ≥ N, u n = v n
⊢ ∀ (n : ℕ), ‖v n‖ ≤ ?m.115 * r ^ n

Tactic:
·

Goal state after:
α : Type u_1
inst✝ : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
v : ℕ → α := ⋯
hC : 0 ≤ C
this : ∀ n ≥ N, u n = v n
⊢ ℝ
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case refine_2
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : ∃ i, (IsCompact i.1 ∧ p i.2) ∧ {f | MapsTo (⇑f) i.1 (U i.2)} ⊆ s
⊢ s ∈ 𝓝 (const X c)

Tactic:
·

Goal state after:
case refine_2
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : ∃ i, (IsCompact i.1 ∧ p i.2) ∧ {f | MapsTo (⇑f) i.1 (U i.2)} ⊆ s
⊢ s ∈ 𝓝 (const X c)
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

pp: case neg
α : 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
⊢ ‖u n‖ ≤ C * r ^ n

Tactic:
·

Goal state after:
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
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case neg
α : 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
⊢ ‖u n‖ ≤ C * r ^ n

Tactic:
·

Goal state after:
case neg
α : 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
⊢ ‖u n‖ ≤ C * r ^ n
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case pos
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : 0 ≤ r
⊢ Summable f

pp: case neg
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
⊢ Summable f

Tactic:
·

Goal state after:
case pos
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : 0 ≤ r
⊢ Summable f
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
⊢ Continuous[_, inst✝] ({1}.piecewise (const (↑I) y) (const (↑I) x))

pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
t : ↑I
⊢ { toFun := {1}.piecewise (const (↑I) y) (const (↑I) x), continuous_toFun := ?refine_1, source' := ⋯, target' := ⋯ }
      t ∈
    F

Tactic:
·

Goal state after:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
⊢ Continuous[_, inst✝] ({1}.piecewise (const (↑I) y) (const (↑I) x))
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
t : ↑I
⊢ { toFun := {1}.piecewise (const (↑I) y) (const (↑I) x), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } t ∈ F

Tactic:
·

Goal state after:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
t : ↑I
⊢ { toFun := {1}.piecewise (const (↑I) y) (const (↑I) x), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } t ∈ F
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent x → z ∈ pathComponent y

pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent y → z ∈ pathComponent x

Tactic:
·

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent x → z ∈ pathComponent y
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent y → z ∈ pathComponent x

Tactic:
·

Goal state after:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent y → z ∈ pathComponent x
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case neg
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
⊢ Summable f

Tactic:
·

Goal state after:
case neg
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
⊢ Summable f
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
⊢ pathComponentIn F x = F

pp: case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn F x = F
⊢ ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y

Tactic:
·

Goal state after:
case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
⊢ pathComponentIn F x = F
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn F x = F
⊢ ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y

Tactic:
·

Goal state after:
case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn F x = F
⊢ ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case right.inl
X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
y : X
yU : y ∈ U
⊢ JoinedIn (U ∪ V) x y

pp: case right.inr
X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
y : X
yV : y ∈ V
⊢ JoinedIn (U ∪ V) x y

Tactic:
·

Goal state after:
case right.inl
X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
y : X
yU : y ∈ U
⊢ JoinedIn (U ∪ V) x y
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case right.inr
X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
y : X
yV : y ∈ V
⊢ JoinedIn (U ∪ V) x y

Tactic:
·

Goal state after:
case right.inr
X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
y : X
yV : y ∈ V
⊢ JoinedIn (U ∪ V) x y
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case mp
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
⊢ (∃ f, Tendsto F l (𝓝 f)) → ∀ (s : Set X), IsCompact s → ∃ f, Tendsto (fun i ↦ restrict s (F i)) l (𝓝 f)

pp: case mpr
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
⊢ (∀ (s : Set X), IsCompact s → ∃ f, Tendsto (fun i ↦ restrict s (F i)) l (𝓝 f)) → ∃ f, Tendsto F l (𝓝 f)

Tactic:
·

Goal state after:
case mp
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
⊢ (∃ f, Tendsto F l (𝓝 f)) → ∀ (s : Set X), IsCompact s → ∃ f, Tendsto (fun i ↦ restrict s (F i)) l (𝓝 f)
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case mpr
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
⊢ (∀ (s : Set X), IsCompact s → ∃ f, Tendsto (fun i ↦ restrict s (F i)) l (𝓝 f)) → ∃ f, Tendsto F l (𝓝 f)

Tactic:
·

Goal state after:
case mpr
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
⊢ (∀ (s : Set X), IsCompact s → ∃ f, Tendsto (fun i ↦ restrict s (F i)) l (𝓝 f)) → ∃ f, Tendsto F l (𝓝 f)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case convert_2
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), N₀ ≤ b → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n ↦ f (n + N)) atTop (𝓝 0)
⊢ 0 < ((fun a ↦ ‖a‖) ∘ fun n ↦ f (n + N)) 0

pp: case convert_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), N₀ ≤ b → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n ↦ f (n + N)) atTop (𝓝 0)
⊢ ∀ (n : ℕ), r * ((fun a ↦ ‖a‖) ∘ fun n ↦ f (n + N)) n ≤ ((fun a ↦ ‖a‖) ∘ fun n ↦ f (n + N)) (n + 1)

Tactic:
·

Goal state after:
case convert_2
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), N₀ ≤ b → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n ↦ f (n + N)) atTop (𝓝 0)
⊢ 0 < ((fun a ↦ ‖a‖) ∘ fun n ↦ f (n + N)) 0
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case convert_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), N₀ ≤ b → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n ↦ f (n + N)) atTop (𝓝 0)
⊢ ∀ (n : ℕ), r * ((fun a ↦ ‖a‖) ∘ fun n ↦ f (n + N)) n ≤ ((fun a ↦ ‖a‖) ∘ fun n ↦ f (n + N)) (n + 1)

Tactic:
·

Goal state after:
case convert_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), N₀ ≤ b → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n ↦ f (n + N)) atTop (𝓝 0)
⊢ ∀ (n : ℕ), r * ((fun a ↦ ‖a‖) ∘ fun n ↦ f (n + N)) n ≤ ((fun a ↦ ‖a‖) ∘ fun n ↦ f (n + N)) (n + 1)
Module: Mathlib.Topology.Path

Goal state before:
pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ↑t ≤ 1 / 2
⊢ γ ⟨2 * ↑(σ t), ⋯⟩ = γ' (σ ⟨2 * ↑t, ⋯⟩)

pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ¬↑t ≤ 1 / 2
⊢ γ ⟨2 * ↑(σ t), ⋯⟩ = γ (σ ⟨2 * ↑t - 1, ⋯⟩)

pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ' (σ ⟨2 * ↑t, ⋯⟩)

pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ (σ ⟨2 * ↑t - 1, ⋯⟩)

Tactic:
·

Goal state after:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ↑t ≤ 1 / 2
⊢ γ ⟨2 * ↑(σ t), ⋯⟩ = γ' (σ ⟨2 * ↑t, ⋯⟩)
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := ⋯
⊢ PathConnectedSpace X → Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)

pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := ⋯
⊢ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X) → PathConnectedSpace X

Tactic:
·

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := ⋯
⊢ PathConnectedSpace X → Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := ⋯
⊢ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X) → PathConnectedSpace X

Tactic:
·

Goal state after:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := ⋯
⊢ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X) → PathConnectedSpace X
Module: Mathlib.Topology.Path

Goal state before:
pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ¬↑t ≤ 1 / 2
⊢ γ ⟨2 * ↑(σ t), ⋯⟩ = γ (σ ⟨2 * ↑t - 1, ⋯⟩)

pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ' (σ ⟨2 * ↑t, ⋯⟩)

pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ (σ ⟨2 * ↑t - 1, ⋯⟩)

Tactic:
·

Goal state after:
case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ¬↑t ≤ 1 / 2
⊢ γ ⟨2 * ↑(σ t), ⋯⟩ = γ (σ ⟨2 * ↑t - 1, ⋯⟩)