mathlib-initiative/mathlib-tactics huggingface dataset:
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:
push Not at H
    exact h _ H

Goal state after:
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
⊢ CauchySeq fun n ↦ ∑ k ∈ Finset.range (n + 1), u k

Tactic:
by

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
r : X
f : C(Y, Z)
K : Set Y
hK : IsCompact K
U : Set (X × Z)
hU : IsOpen[instTopologicalSpaceProd] U
H : MapsTo (⇑((const Y (r, f).1).prodMk (r, f).2)) K U
⊢ {r} ×ˢ (⇑f '' K) ⊆ U

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
h : CauchySeq fun n ↦ ∑ k ∈ Finset.range n, f k
⊢ ∃ C, ∀ (n : ℕ), ‖f n‖ ≤ C

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: M : Type u_4
inst✝² : MulOneClass M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l l' : List M
h : List.Forall₂ Joined l l'
⊢ Joined l.prod l'.prod

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ Surjective mk

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
motive : ZerothHomotopy X → Prop
mk : ∀ (x : X), motive (ZerothHomotopy.mk x)
x : ZerothHomotopy X
⊢ motive x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
r : X
f : C(Y, Z)
K : Set Y
hK : IsCompact K
U : Set (X × Z)
hU : IsOpen[instTopologicalSpaceProd] U
H : MapsTo (⇑((const Y (r, f).1).prodMk (r, f).2)) K U
V : Set X
W : Set Z
hV : IsOpen[inst✝²] V
hW : IsOpen[inst✝] W
hrV : {r} ⊆ V
hKW : ⇑f '' K ⊆ W
hVW : V ×ˢ W ⊆ U
⊢ r ∈ V

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
γ : Path x y
γ_in : ∀ (t : ↑I), γ t ∈ F
⊢ γ 0 ∈ F ∧ γ 1 ∈ F

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ x ∈ F ∧ y ∈ F

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ Continuous[_, instTopologicalSpaceSubtype] fun t ↦ ⟨h.somePath t, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ ⟨h.somePath 0, ⋯⟩ = ⟨x, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ ⟨h.somePath 1, ⋯⟩ = ⟨y, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
x_in : x ∈ F
y_in : y ∈ F
h : Joined ⟨x, x_in⟩ ⟨y, y_in⟩
⊢ ∀ (t : ↑I), (h.somePath.map ⋯) t ∈ F

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ JoinedIn univ x y ↔ Joined x y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ JoinedIn F y x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
F : Set X
hxy : JoinedIn F x y
hyz : JoinedIn F y z
⊢ JoinedIn F x z

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
⊢ { toFun := {1}.piecewise (const (↑I) y) (const (↑I) x), continuous_toFun := ?m.32 }.toFun 0 = x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
⊢ { toFun := {1}.piecewise (const (↑I) y) (const (↑I) x), continuous_toFun := ?m.32 }.toFun 1 = y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
⊢ Continuous[instTopologicalSpaceProd, _] fun p ↦ (const Y p.1).prodMk p.2

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
⊢ JoinedIn F x y

Tactic:
by

Goal state after:
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 : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : ↑I → X
hγ'F : ∀ (t : ↑I), γ' t ∈ F
hγ' : ∀ (t : ↑I), f (γ' t) = γ t
⊢ x ⤳ γ' 0

Tactic:
by

Goal state after:
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 : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : ↑I → X
hγ'F : ∀ (t : ↑I), γ' t ∈ F
hγ' : ∀ (t : ↑I), f (γ' t) = γ t
h₀ : x ⤳ γ' 0
⊢ γ' 1 ⤳ y

Tactic:
by

Goal state after:
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 : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : ↑I → X
hγ'F : ∀ (t : ↑I), γ' t ∈ F
hγ' : ∀ (t : ↑I), f (γ' t) = γ t
h₀ : x ⤳ γ' 0
h₁ : γ' 1 ⤳ y
⊢ JoinedIn F (γ' 0) (γ' 1)

Tactic:
by

Goal state after:
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 : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
⊢ JoinedIn (f '' F) (f x) (f y) ↔ JoinedIn F x y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
⊢ pathComponent x = pathComponent y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : y ∈ pathComponent x
⊢ (Joined.somePath h) 0 = x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : y ∈ pathComponent x
⊢ (Joined.somePath h) 1 = y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ ⋃ y ∈ connectedComponent x, pathComponent y = connectedComponent x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ pathComponentIn univ x = pathComponent x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ∈ pathComponentIn F y
⊢ pathComponentIn F x = pathComponentIn F y

Tactic:
by

Goal state after:
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
M : Type u_4
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m₁ m₂ : M
hm₁ : m₁ ∈ pathComponent 1
hm₂ : m₂ ∈ pathComponent 1
⊢ m₁ * m₂ ∈ pathComponent 1

Tactic:
by

Goal state after:
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
G : Type u_4
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
g : G
hg : g ∈ (Submonoid.pathComponentOne G).carrier
⊢ g⁻¹ ∈ (Submonoid.pathComponentOne G).carrier

Tactic:
by

Goal state after:
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
G : Type u_4
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
x✝¹ : G
x✝ : x✝¹ ∈ Subgroup.pathComponentOne G
g : G
γ : Path 1 x✝¹
⊢ Continuous[_, inst✝¹] fun x ↦ g * γ x * g⁻¹

Tactic:
by

Goal state after:
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
G : Type u_4
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
x✝¹ : G
x✝ : x✝¹ ∈ Subgroup.pathComponentOne G
g : G
γ : Path 1 x✝¹
⊢ { toFun := fun x ↦ g * γ x * g⁻¹, continuous_toFun := ⋯ }.toFun 0 = 1

Tactic:
by

Goal state after:
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
G : Type u_4
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
x✝¹ : G
x✝ : x✝¹ ∈ Subgroup.pathComponentOne G
g : G
γ : Path 1 x✝¹
⊢ { toFun := fun x ↦ g * γ x * g⁻¹, continuous_toFun := ⋯ }.toFun 1 = g * x✝¹ * g⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactPair Y Z
⊢ Continuous fun x ↦ x.2.comp x.1

Tactic:
by

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

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

Tactic:
by

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

Tactic:
ext y
    exact ⟨fun hy => hy.mem.2, @h _⟩

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
⊢ IsPathConnected F ↔ ∃ x ∈ F, pathComponentIn F x = F

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Set X
hF : IsPathConnected F
f : X → Y
hf : ContinuousOn f F
⊢ IsPathConnected (f '' F)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: G : Type u_4
inst✝² : InvolutiveInv G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousInv G
s : Set G
hs : IsPathConnected s
a : G
ha_mem : a ∈ s
ha : ∀ ⦃y : G⦄, y ∈ s → JoinedIn s a y
x : G
hx : x ∈ s⁻¹
⊢ JoinedIn s⁻¹ a⁻¹ x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Set X
f : X → Y
hf : IsInducing f
⊢ IsPathConnected F ↔ IsPathConnected (f '' F)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace T
K : Set X
U : Set Y
inst✝ : LocallyCompactPair X Y
⊢ Continuous[instTopologicalSpaceProd, inst✝³] fun fx ↦ fx.1 fx.2

Tactic:
by

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace T
K : Set X
U✝ : Set Y
x : X
U : Set Y
hU : IsOpen[inst✝²] U
⊢ IsOpen ((fun f ↦ f x) ⁻¹' U)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
h : ⇑f ⤳ ⇑g
this : ∀ (K : Set X), IsCompact K → ∀ (U : Set Y), IsOpen[inst✝] U → MapsTo (⇑g) K U → MapsTo (⇑f) K U
⊢ f ⤳ g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsPathConnected (⇑h ⁻¹' s) ↔ IsPathConnected s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
⊢ ⇑f ⤳ ⇑g ↔ f ⤳ g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ IsPathConnected {x}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
⊢ Inseparable ⇑f ⇑g ↔ Inseparable f g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
F : Set X
h : x ∈ F
x✝¹ : X
x✝ : x✝¹ ∈ pathComponentIn F x
γ : Path x x✝¹
hγ : ∀ (t : ↑I), γ t ∈ F
t t' : ↑I
⊢ min (max (↑t') 0) ↑t ∈ Icc 0 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace T
K : Set X
U : Set Y
inst✝ : R0Space Y
f g : C(X, Y)
h : f ⤳ g
⊢ g ⤳ f

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
F : Set X
h : x ∈ F
x✝¹ : X
x✝ : x✝¹ ∈ pathComponentIn F x
γ : Path x x✝¹
hγ : ∀ (t : ↑I), γ t ∈ F
⊢ JoinedIn (pathComponentIn F x) x x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ IsPathConnected (pathComponent x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
hUV : (U ∩ V).Nonempty
⊢ IsPathConnected (U ∪ V)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U W : Set X
hW : IsPathConnected W
hWU : W ⊆ U
⊢ IsPathConnected (Subtype.val ⁻¹' W)

Tactic:
by

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 z : X
ι : Type u_3
γ₁ γ₂ : Path x y
h : (fun γ ↦ ⇑γ.toContinuousMap) γ₁ = (fun γ ↦ ⇑γ.toContinuousMap) γ₂
⊢ γ₁ = γ₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace T
K : Set X
U : Set Y
inst✝ : RegularSpace Y
f : C(X, Y)
⊢ (𝓝 f).lift' closure ≤ 𝓝 f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ ∀ {γ₁ γ₂ : Path x y}, ⇑γ₁ = ⇑γ₂ → γ₁ = γ₂

Tactic:
by

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 z : X
ι : Type u_3
γ✝ γ : Path x y
⊢ Continuous[_, inst✝¹] (⇑γ ∘ σ)

Tactic:
by

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 z : X
ι : Type u_3
γ✝ γ : Path x y
⊢ (⇑γ ∘ σ) 0 = y

Tactic:
by

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 z : X
ι : Type u_3
γ✝ γ : Path x y
⊢ (⇑γ ∘ σ) 1 = x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ γ.symm.symm = γ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ γ.extend 0 = x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ γ.extend 1 = y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ compactOpen = ⨅ K, ⨅ (_ : IsCompact K), induced (restrict K) compactOpen

Tactic:
by

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 z : X
ι : Type u_3
γ✝ γ : Path x y
⊢ ContinuousOn ⇑γ.extend I

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ ofLine ⋯ ⋯ ⋯ = γ

Tactic:
by

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 z : X
ι : Type u_3
γ✝ γ : Path x y
γ' : Path y z
⊢ ∀ (x_1 : ℝ), id x_1 = 1 / 2 → γ.extend (2 * x_1) = γ'.extend (2 * x_1 - 1)

Tactic:
by

Goal state after:
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 = ⨅ s, ⨅ (_ : IsCompact s), comap (restrict s) (𝓝 (restrict s f))

Tactic:
by

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 z : X
ι : Type u_3
γ✝ γ : Path x y
γ' : Path y z
⊢ Continuous[_, inst✝¹] ((fun t ↦ if t ≤ 1 / 2 then γ.extend (2 * t) else γ'.extend (2 * t - 1)) ∘ Subtype.val)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
l : Filter ι
F : ι → C(X, Y)
f : C(X, Y)
⊢ Tendsto F l (𝓝 f) ↔ ∀ (K : Set X), IsCompact K → Tendsto (fun i ↦ restrict K (F i)) l (𝓝 (restrict K f))

Tactic:
by

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 z : X
ι : Type u_3
γ✝ γ : Path x y
γ' : Path y z
⊢ ((fun t ↦ if t ≤ 1 / 2 then γ.extend (2 * t) else γ'.extend (2 * t - 1)) ∘ Subtype.val) 0 = x

Tactic:
by

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 z : X
ι : Type u_3
γ✝ γ : Path x y
γ' : Path y z
⊢ ((fun t ↦ if t ≤ 1 / 2 then γ.extend (2 * t) else γ'.extend (2 * t - 1)) ∘ Subtype.val) 1 = z

Tactic:
by

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: 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 : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i ↦ restrict s (F i)) l (𝓝 (f s a))
⊢ ∀ (s₁ : Set X) (hs₁ : IsCompact s₁) (s₂ : Set X) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
⊢ ∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
⊢ ∃ γ t, (∀ (t : ↑I), γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), γ (t i) = p i

Tactic:
by

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

Goal state before:
pp: α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∃ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, r * ‖f n‖ ≤ ‖f (n + 1)‖
⊢ ¬Summable f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: 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
⊢ ↑t = 1 / 2

Tactic:
by

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: 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)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
y : Y
s : Set X
⊢ ⇑(coev X Y y) '' s = {y} ×ˢ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace T
K : Set X
U : Set Y
f : C(X × Y, Z)
a : X
⊢ Continuous[inst✝², instTopologicalSpaceProd] (Prod.mk a)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ PathConnectedSpace X ↔ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ PathConnectedSpace X ↔ IsPathConnected univ

Tactic:
by

Goal state after: