mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
x : ↑(Icc a c)
hx : ↑x ≤ b
fg : { fg // fg.1 ⊤ = fg.2 ⊥ }
⊢ (concatCM fg) x = (↑fg).1 ⟨↑x, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
x : X
hxV : x ∈ ⇑f ⁻¹' V
⊢ ∃ U ∈ countableBasis X, x ∈ U ∧ U ⊆ ⇑f ⁻¹' V

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Convenient.Localization

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
⊢ (morphismPropertyWithGeneratedByTopologyEquiv X).IsInvertedBy (toContinuousGeneratedByCat X)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Convenient.Localization

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
x✝ : TopCat
⊢ morphismPropertyWithGeneratedByTopologyEquiv X (ContinuousGeneratedByCat.adj.counit.app x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Convenient.Localization

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
⊢ (morphismPropertyWithGeneratedByTopologyEquiv X).IsInvertedBy toGeneratedByTopCat

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Convenient.Localization

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
x✝ : TopCat
⊢ morphismPropertyWithGeneratedByTopologyEquiv X (GeneratedByTopCat.adj.counit.app x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
⊢ SecondCountableTopology C(X, Y)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Convenient.HomSpace

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝³ : (i : ι) → TopologicalSpace (X i)
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
A : Type u_1
inst✝ : TopologicalSpace A
φ : A → ContinuousMapGeneratedBy X Z T
⊢ Continuous[inst✝, _] φ ↔ ∀ (i : ι) (f : C(X i, Z)), Continuous[inst✝, _] (precomp f ∘ φ)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Convenient.HomSpace

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Z : Type v'
inst✝¹ : TopologicalSpace Z
T : Type v''
inst✝ : TopologicalSpace T
i : ι
f : C(X i, Z)
⊢ Continuous (precomp f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Convenient.HomSpace

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i : ι), LocallyCompactSpace (X i)
g : Z → ContinuousMapGeneratedBy X Y T
⊢ ContinuousGeneratedBy X g ↔
    ∀ ⦃i₁ : ι⦄ (f₁ : C(X i₁, Z)) ⦃i₂ : ι⦄ (f₂ : C(X i₂, Y)),
      Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦
        match x with
        | (x₁, x₂) => (g (f₁ x₁)) (f₂ x₂)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.T0Sierpinski

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen[t] u
⊢ (fun x ↦ x ∈ { carrier := u, is_open' := h }) ⁻¹' {True} = u

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.T0Sierpinski

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
⊢ t = ⨅ u, induced (fun x ↦ x ∈ u) sierpinskiSpace

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.T0Sierpinski

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsInducing ⇑(productOfMemOpens X)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.T0Sierpinski

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
⊢ Function.Injective ⇑(productOfMemOpens X)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Convenient.HomSpace

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
⊢ ContinuousGeneratedBy X g ↔
    ∀ (i₁ : ι) (f₁ : C(X i₁, Z)) (i₂ : ι) (f₂ : C(X i₂, Y)),
      Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦
        match x with
        | (x₁, x₂) => g (f₂ x₂, f₁ x₁)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Convenient.HomSpace

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝⁵ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝⁴ : TopologicalSpace Y
Z : Type v'
inst✝³ : TopologicalSpace Z
T : Type v''
inst✝² : TopologicalSpace T
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : ContinuousMapGeneratedBy X (Y × Z) T
⊢ ContinuousGeneratedBy X fun z ↦ g.comp { toFun := fun y ↦ (y, z), prop := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Convenient.HomSpace

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝⁵ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝⁴ : TopologicalSpace Y
Z : Type v'
inst✝³ : TopologicalSpace Z
T : Type v''
inst✝² : TopologicalSpace T
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : ContinuousMapGeneratedBy X Z (ContinuousMapGeneratedBy X Y T)
⊢ ContinuousGeneratedBy X fun x ↦ (g x.2) x.1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
s : Set α
⊢ IsOpen {l | s ∈ l}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
s t : Set α
l : Filter α
hl : l ∈ (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
⊢ (Iic ∘ 𝓟) (s ∩ t) = Iic (𝓟 s) ∩ Iic (𝓟 t)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
⊢ ∀ t₁ ∈ range (Iic ∘ 𝓟), ∀ t₂ ∈ range (Iic ∘ 𝓟), ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ range (Iic ∘ 𝓟), x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
s : Set (Filter α)
⊢ (∃ S ⊆ range (Iic ∘ 𝓟), s = ⋃₀ S) ↔ ∃ T, s = ⋃ t ∈ T, Iic (𝓟 t)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
l : Filter α
⊢ ⨅ s ∈ {s | l ∈ s ∧ s ∈ range (Iic ∘ 𝓟)}, 𝓟 s = l.lift' (Iic ∘ 𝓟)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
l : Filter α
⊢ 𝓝 l = l.lift' fun s ↦ {l' | s ∈ l'}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
β : Type u_3
la : Filter α
lb : Filter β
f : α → Filter β
⊢ Tendsto f la (𝓝 lb) ↔ ∀ s ∈ lb, ∀ᶠ (a : α) in la, s ∈ f a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ (𝓝 l).HasBasis p fun i ↦ Iic (𝓟 (s i))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: X : Type u_4
l : Filter X
⊢ Tendsto pure l (𝓝 l)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ (𝓝 l).HasBasis p fun i ↦ {l' | s i ∈ l'}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
⊢ 𝓝 ⊥ = pure ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
⊢ 𝓝 ⊤ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
x : α
⊢ 𝓝 (pure x) = 𝓟 {⊥, pure x}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ 𝓝 (⨅ i, f i) = ⨅ i, 𝓝 (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
l₁ l₂ : Filter α
⊢ 𝓝 (l₁ ⊓ l₂) = 𝓝 l₁ ⊓ 𝓝 l₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
l : Filter α
⊢ ⋂₀ {s | s ∈ 𝓝 l} = Iic l

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
l₁ l₂ : Filter α
⊢ 𝓝 l₁ ≤ 𝓝 l₂ ↔ l₁ ≤ l₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
s : Set (Filter α)
l : Filter α
⊢ l ∈ interior s ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
s : Set (Filter α)
l : Filter α
⊢ l ∈ closure s ↔ ∀ t ∈ l, ∃ l' ∈ s, t ∈ l'

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
l : Filter α
⊢ closure {l} = Ici l

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
l₁ l₂ : Filter α
⊢ l₁ ⤳ l₂ ↔ l₁ ≤ l₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
⊢ 𝓝 atTop = ⨅ x, 𝓟 (Iic (𝓟 (Ici x)))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : Preorder β
l : Filter α
f : α → Filter β
⊢ Tendsto f l (𝓝 atTop) ↔ ∀ (y : β), ∀ᶠ (a : α) in l, Ici y ∈ f a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: X : Type u_4
inst✝ : TopologicalSpace X
x : X
⊢ 𝓝 (𝓝 x) = ⨅ s, ⨅ (_ : IsOpen[inst✝] s), ⨅ (_ : x ∈ s), 𝓟 (Iic (𝓟 s))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: X : Type u_4
inst✝ : TopologicalSpace X
x : X
⊢ ⨅ s, ⨅ (_ : IsOpen[inst✝] s), ⨅ (_ : x ∈ s), 𝓟 s = comap 𝓝 (𝓝 (𝓝 x))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
⊢ some '' Metric.eball a r = Metric.eball (some a) r

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝ : α
⊢ edist (some val✝) (some val✝) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝¹ val✝ : α
⊢ edist (some val✝¹) (some val✝) = edist (some val✝) (some val✝¹)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝ : α
⊢ edist (some val✝) none = edist none (some val✝)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝ : α
⊢ edist none (some val✝) = edist (some val✝) none

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
⊢ edist none none = edist none none

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝² val✝¹ val✝ : α
⊢ edist (some val✝²) (some val✝) ≤ edist (some val✝²) (some val✝¹) + edist (some val✝¹) (some val✝)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Germ

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X✝
f✝ g✝ : X✝ → Y
A : Set X✝
x✝ : X✝
X : Type u_4
α : Type u_5
inst✝ : TopologicalSpace X
x : X
φ : (𝓝 x).Germ α
f g : X → α
h : ((𝓝 x).germSetoid α) f g
⊢ f x = g x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝¹ val✝ : α
⊢ edist none (some val✝) ≤ edist none (some val✝¹) + edist (some val✝¹) (some val✝)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝¹ val✝ : α
⊢ edist (some val✝¹) (some val✝) ≤ edist (some val✝¹) none + edist none (some val✝)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝ : α
⊢ edist none (some val✝) ≤ edist none none + edist none (some val✝)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝¹ val✝ : α
⊢ edist (some val✝¹) none ≤ edist (some val✝¹) (some val✝) + edist (some val✝) none

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝ : α
⊢ edist none none ≤ edist none (some val✝) + edist (some val✝) none

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝ : α
⊢ edist (some val✝) none ≤ edist (some val✝) none + edist none none

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
⊢ edist none none ≤ edist none none + edist none none

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
r : ℝ≥0∞
hr : 0 < r
⊢ Metric.eball none r = {none}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝ : TopologicalSpace X
f g : X → Y
A✝ : Set X
x✝ : X
P : (x : X) → (𝓝 x).Germ Y → Prop
A : Set X
x : X
φ : (𝓝 x).Germ Y
⊢ ∀ (f f' : X → Y), f =ᶠ[𝓝 x] f' → (∀ᶠ (y : X) in 𝓝 x, P y ↑f) → ∀ᶠ (y : X) in 𝓝 x, P y ↑f'

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
s : Set (Option α)
so : IsOpen[inst✝] s
x : Option α
xs : x ∈ s
this : ∃ ε > 0, Metric.eball x ε ⊆ s
⊢ ∃ ε > 0, Metric.eball x ε ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
s : Set (Option α)
so : IsOpen[inst✝] s
x : Option α
xs : none ∈ s
⊢ 1 > 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
s : Set (Option α)
so : IsOpen[inst✝] s
x : Option α
xs : none ∈ s
⊢ Metric.eball none 1 ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
s : Set (Option α)
so : IsOpen[inst✝] s
⊢ IsOpen[(uniformSpaceOfEDist edist ⋯ ⋯ ⋯).toTopologicalSpace] s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f g : X → Y
A : Set X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : ∀ᶠ (x : X) in 𝓝ˢ A, P x ↑f
h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z
⊢ ∀ᶠ (x : X) in 𝓝ˢ A, P x ↑g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f g : X → Y
A : Set X
x : X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : RestrictGermPredicate P A x ↑f
h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z
⊢ RestrictGermPredicate P A x ↑g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
A : Set X
P : (x : X) → (𝓝 x).Germ Y → Prop
⊢ (∀ (x : X), RestrictGermPredicate P A x ↑f) ↔ ∀ᶠ (x : X) in 𝓝ˢ A, P x ↑f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Convenient.OpenClosed

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst✝ : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst✝²] U
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Opens (X a.fst) := fun a ↦ { carrier := ⇑a.snd ⁻¹' U, is_open' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑U := fun a ↦ U.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
this :
  ∀ (V : Set ↑U),
    (∀ (a : (i : ι) × C(X i, Y)), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
      IsOpen[instTopologicalSpaceSubtype] V
⊢ IsGeneratedBy X ↑U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x✝¹ : Option α
r : ℝ≥0∞
x : α
s' : Set α
s'o : IsOpen[t] s'
y : Option α
z : α
s's : z ∈ s' ↔ edist z x < r
yh : edist (some z) (some x) < ∞
x✝ : edist (some z) (some x) < r
⊢ z ∈ s' ∧ some z = some z

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), (↑f).IsConstant
s : Set Y
a : X
ha : a ∈ f ⁻¹' s
b : Y
hb : f =ᶠ[𝓝 a] fun x ↦ b
x : X
hx : x ∈ {x | (fun x ↦ f x = (fun x ↦ b) x) x}
⊢ x ∈ f ⁻¹' s

Tactic:
have : f x = f a := (mem_of_mem_nhds hb) ▸ hx

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), (↑f).IsConstant
s : Set Y
a : X
ha : a ∈ f ⁻¹' s
b : Y
hb : f =ᶠ[𝓝 a] fun x ↦ b
x : X
hx : x ∈ {x | (fun x ↦ f x = (fun x ↦ b) x) x}
this : f x = f a
⊢ x ∈ f ⁻¹' s
Module: Mathlib.Topology.Convenient.OpenClosed

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst✝ : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst✝²] U
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Opens (X a.fst) := fun a ↦ { carrier := ⇑a.snd ⁻¹' U, is_open' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑U := fun a ↦ U.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set ↑U
hV : ∀ (a : (i : ι) × C(X i, Y)), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' V)
⊢ Subtype.val '' V ⊆ U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), (↑f).IsConstant
⊢ IsLocallyConstant f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
i : PreconnectedSpace X
h : ∀ (x : X), (↑f).IsConstant
x x' : X
⊢ x ∈ univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Convenient.OpenClosed

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst✝ : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst✝²] U
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Opens (X a.fst) := fun a ↦ { carrier := ⇑a.snd ⁻¹' U, is_open' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑U := fun a ↦ U.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set ↑U
hV : ∀ (a : (i : ι) × C(X i, Y)), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' V)
⊢ V = Subtype.val ⁻¹' Subtype.val '' V

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
i : PreconnectedSpace X
h : ∀ (x : X), (↑f).IsConstant
x x' : X
⊢ x' ∈ univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
x : X
s : Set X
h : ∀ x ∈ s, (↑f).IsConstant
hs : IsPreconnected s
x' : X
x_in : x ∈ s
x'_in : x' ∈ s
⊢ f x = f x'

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
⊢ ∀ (x : Option α) (r : ℝ≥0∞), IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' Metric.eball x r)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Hom.Open

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : α →CO β
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
map_open'✝ : IsOpenMap { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }.toFun
h :
  (fun f ↦ f.toFun) { toFun := toFun✝, continuous_toFun := continuous_toFun✝, map_open' := map_open'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, continuous_toFun := continuous_toFun✝, map_open' := map_open'✝ } = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := g

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
toFun✝¹ : α → β
continuous_toFun✝¹ : Continuous toFun✝¹
map_open'✝¹ : IsOpenMap { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹ }.toFun
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
map_open'✝ : IsOpenMap { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }.toFun
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹, map_open' := map_open'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, continuous_toFun := continuous_toFun✝, map_open' := map_open'✝ }
⊢ { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹, map_open' := map_open'✝¹ } =
    { toFun := toFun✝, continuous_toFun := continuous_toFun✝, map_open' := map_open'✝ }
Module: Mathlib.Topology.Hom.Open

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : α →CO β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Hom.Open

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β →CO γ
f₁ f₂ : α →CO β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
by

Goal state after: