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

Goal state before:
pp: case pos
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
f : (i : ι) → X i
hf : f ∈ (↑i).pi t
c : (a : ι) → Set (X a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
a : ι
h✝ : a ∈ i
⊢ (↑i).piecewise t c a ∈ g a

pp: case neg
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
f : (i : ι) → X i
hf : f ∈ (↑i).pi t
c : (a : ι) → Set (X a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
a : ι
h✝ : a ∉ i
⊢ (↑i).piecewise t c a ∈ g a

Tactic:
<;>

Goal state after:
case pos
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
f : (i : ι) → X i
hf : f ∈ (↑i).pi t
c : (a : ι) → Set (X a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
a : ι
h✝ : a ∈ i
⊢ (↑i).piecewise t c a ∈ g a

case neg
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
f : (i : ι) → X i
hf : f ∈ (↑i).pi t
c : (a : ι) → Set (X a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
a : ι
h✝ : a ∉ i
⊢ (↑i).piecewise t c a ∈ g a
Module: Mathlib.Topology.Bases

Goal state before:
pp: case mp
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
⊢ (∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i) →
    ∃ U F, (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i

pp: case mpr
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
⊢ (∃ U F, (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i) →
    ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i

Tactic:
<;>

Goal state after:
case mp
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
⊢ (∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i) →
    ∃ U F, (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i

case mpr
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
⊢ (∃ U F, (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i) →
    ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case inr
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen[inst✝ i] s
j : ι
hne : j ≠ i
⊢ IsOpen[inst✝ j] (Sigma.mk j ⁻¹' Sigma.mk i '' s)

Tactic:
rw [preimage_image_sigmaMk_of_ne hne]

Goal state after:
case inr
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen[inst✝ i] s
j : ι
hne : j ≠ i
⊢ IsOpen[inst✝ j] ∅
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case inr
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed[inst✝ i] s
j : ι
hne : j ≠ i
⊢ IsClosed[inst✝ j] (Sigma.mk j ⁻¹' Sigma.mk i '' s)

Tactic:
rw [preimage_image_sigmaMk_of_ne hne]

Goal state after:
case inr
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed[inst✝ i] s
j : ι
hne : j ≠ i
⊢ IsClosed[inst✝ j] ∅
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: X : Type u_4
inst✝ : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
hf : LocallyFinite fun n ↦ {x | f (n + 1) x ≠ f n x}
⊢ ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.1 p.2 = F p.2

Tactic:
choose U hUx hU using hf

Goal state after:
X : Type u_4
inst✝ : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | ((fun n ↦ {x | f (n + 1) x ≠ f n x}) i ∩ U x).Nonempty}.Finite
⊢ ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.1 p.2 = F p.2
Module: Mathlib.Data.Set.Subset

Goal state before:
pp: α : Type u_2
A : Set α
S : Set (Set α)
⊢ A ↓∩ ⋃₀ S = ⋃ a ∈ S, A ↓∩ a

Tactic:
simp_rw [sUnion_eq_biUnion, preimage_iUnion]

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case false
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (bif false then s else t)

pp: case true
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (bif true then s else t)

Tactic:
<;>

Goal state after:
case false
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (bif false then s else t)

case true
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (bif true then s else t)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case refine_1
X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst✝¹] (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen[inst✝¹] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
i j k : ι
hki : V i ⊇ V k
hkj : V j ⊇ V k
x : X
⊢ x ∈ V k ∩ Wᶜ → x ∈ V i ∩ Wᶜ

pp: case refine_2
X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst✝¹] (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen[inst✝¹] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
i j k : ι
hki : V i ⊇ V k
hkj : V j ⊇ V k
x : X
⊢ x ∈ V k ∩ Wᶜ → x ∈ V j ∩ Wᶜ

Tactic:
<;>

Goal state after:
case refine_1
X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst✝¹] (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen[inst✝¹] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
i j k : ι
hki : V i ⊇ V k
hkj : V j ⊇ V k
x : X
⊢ x ∈ V k ∩ Wᶜ → x ∈ V i ∩ Wᶜ

case refine_2
X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst✝¹] (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen[inst✝¹] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
i j k : ι
hki : V i ⊇ V k
hkj : V j ⊇ V k
x : X
⊢ x ∈ V k ∩ Wᶜ → x ∈ V j ∩ Wᶜ
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case refine_1
X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst✝¹] (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen[inst✝¹] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
i j k : ι
hki : V i ⊇ V k
hkj : V j ⊇ V k
x : X
⊢ x ∈ V k → x ∉ W → x ∈ V i ∧ x ∉ W

pp: case refine_2
X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst✝¹] (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen[inst✝¹] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
i j k : ι
hki : V i ⊇ V k
hkj : V j ⊇ V k
x : X
⊢ x ∈ V k → x ∉ W → x ∈ V j ∧ x ∉ W

Tactic:
<;>

Goal state after:
case refine_1
X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst✝¹] (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen[inst✝¹] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
i j k : ι
hki : V i ⊇ V k
hkj : V j ⊇ V k
x : X
⊢ x ∈ V k → x ∉ W → x ∈ V i ∧ x ∉ W

case refine_2
X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst✝¹] (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen[inst✝¹] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
i j k : ι
hki : V i ⊇ V k
hkj : V j ⊇ V k
x : X
⊢ x ∈ V k → x ∉ W → x ∈ V j ∧ x ∉ W
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: case hts
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ {a} ⊆ ↑s

pp: case hst
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ ∀ b ∈ s, ∀ c ∈ {a}, b ≤ c → b ∈ {a}

Tactic:
<;>

Goal state after:
case hts
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ {a} ⊆ ↑s

case hst
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ ∀ b ∈ s, ∀ c ∈ {a}, b ≤ c → b ∈ {a}
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s t : UpperSet α
⊢ Codisjoint ↑s ↑t ↔ Disjoint s t

Tactic:
simp [disjoint_iff, codisjoint_iff, SetLike.ext'_iff]

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
⊢ ∀ s_1 ∈ (fun x ↦ closure[inst✝] {x}) '' s, IsClosed[inst✝] s_1

pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
⊢ ⋃₀ ((fun x ↦ closure[inst✝] {x}) '' s) = s

Tactic:
· rintro _ ⟨_, _, rfl⟩; exact isClosed_closure

Goal state after:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
⊢ ⋃₀ ((fun x ↦ closure[inst✝] {x}) '' s) = s
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case hp
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ frontier {x | p x}, f a = g a
hf : ContinuousOn f (closure[inst✝²] {x | p x})
hg : ContinuousOn g (closure[inst✝²] {x | ¬p x})
⊢ ∀ a ∈ univ ∩ frontier {a | p a}, f a = g a

pp: case hf
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ frontier {x | p x}, f a = g a
hf : ContinuousOn f (closure[inst✝²] {x | p x})
hg : ContinuousOn g (closure[inst✝²] {x | ¬p x})
⊢ ContinuousOn f (univ ∩ closure[inst✝²] {a | p a})

pp: case hg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ frontier {x | p x}, f a = g a
hf : ContinuousOn f (closure[inst✝²] {x | p x})
hg : ContinuousOn g (closure[inst✝²] {x | ¬p x})
⊢ ContinuousOn g (univ ∩ closure[inst✝²] {a | ¬p a})

Tactic:
<;>

Goal state after:
case hp
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ frontier {x | p x}, f a = g a
hf : ContinuousOn f (closure[inst✝²] {x | p x})
hg : ContinuousOn g (closure[inst✝²] {x | ¬p x})
⊢ ∀ a ∈ univ ∩ frontier {a | p a}, f a = g a

case hf
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ frontier {x | p x}, f a = g a
hf : ContinuousOn f (closure[inst✝²] {x | p x})
hg : ContinuousOn g (closure[inst✝²] {x | ¬p x})
⊢ ContinuousOn f (univ ∩ closure[inst✝²] {a | p a})

case hg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ frontier {x | p x}, f a = g a
hf : ContinuousOn f (closure[inst✝²] {x | p x})
hg : ContinuousOn g (closure[inst✝²] {x | ¬p x})
⊢ ContinuousOn g (univ ∩ closure[inst✝²] {a | ¬p a})
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case pos
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
hs : Continuous[inst✝, _] fun x ↦ x ∈ s
hs' : Continuous[inst✝, _] fun x ↦ x ∈ s'
x : α
hx : x ∈ t
⊢ x ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (Membership.mem s) (Membership.mem s') x

pp: case neg
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
hs : Continuous[inst✝, _] fun x ↦ x ∈ s
hs' : Continuous[inst✝, _] fun x ↦ x ∈ s'
x : α
hx : x ∉ t
⊢ x ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (Membership.mem s) (Membership.mem s') x

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
hs : Continuous[inst✝, _] fun x ↦ x ∈ s
hs' : Continuous[inst✝, _] fun x ↦ x ∈ s'
x : α
hx : x ∈ t
⊢ x ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (Membership.mem s) (Membership.mem s') x

case neg
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
hs : Continuous[inst✝, _] fun x ↦ x ∈ s
hs' : Continuous[inst✝, _] fun x ↦ x ∈ s'
x : α
hx : x ∉ t
⊢ x ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (Membership.mem s) (Membership.mem s') x
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case mp
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed[topologicalSpace] s
⊢ IsCompact s → ∀ (i : ι), IsCompact (eval i '' s)

pp: case mpr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed[topologicalSpace] s
⊢ (∀ (i : ι), IsCompact (eval i '' s)) → IsCompact s

Tactic:
<;>

Goal state after:
case mp
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed[topologicalSpace] s
⊢ IsCompact s → ∀ (i : ι), IsCompact (eval i '' s)

case mpr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed[topologicalSpace] s
⊢ (∀ (i : ι), IsCompact (eval i '' s)) → IsCompact s
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ (∀ t ⊆ S, ∃ u, IsOpen[inst✝] u ∧ u ∩ S = t) → ∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s

pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ (∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s) → ∀ t ⊆ S, ∃ u, IsOpen[inst✝] u ∧ u ∩ S = t

Tactic:
<;>

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ (∀ t ⊆ S, ∃ u, IsOpen[inst✝] u ∧ u ∩ S = t) → ∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s

case mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ (∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s) → ∀ t ⊆ S, ∃ u, IsOpen[inst✝] u ∧ u ∩ S = t
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
⊢ IsPreirreducible (f '' s)

Tactic:
rintro u v hu hv ⟨_, ⟨⟨x, hx, rfl⟩, hxu⟩⟩ ⟨_, ⟨⟨y, hy, rfl⟩, hyv⟩⟩
  rw [← mem_preimage] at hxu hyv
  rcases continuousOn_iff'.1 hf u hu with ⟨u', hu', u'_eq⟩
  rcases continuousOn_iff'.1 hf v hv with ⟨v', hv', v'_eq⟩
  have := H u' v' hu' hv'
  rw [inter_comm s u', ← u'_eq] at this
  rw [inter_comm s v', ← v'_eq] at this
  rcases this ⟨x, hxu, hx⟩ ⟨y, hyv, hy⟩ with ⟨x, hxs, hxu', hxv'⟩
  refine ⟨f x, mem_image_of_mem f hxs, ?_, ?_⟩
  all_goals
    rw [← mem_preimage]
    apply mem_of_mem_inter_left
    show x ∈ _ ∩ s
    simp [*]

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
inst✝ : IndiscreteTopology X
v : Set X
⊢ v = ∅ ∨ v = univ → ∅.Nonempty → v.Nonempty → (∅ ∩ v).Nonempty

pp: case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
inst✝ : IndiscreteTopology X
u v : Set X
h✝ : u = univ
⊢ v = ∅ ∨ v = univ → u.Nonempty → v.Nonempty → (u ∩ v).Nonempty

Tactic:
<;>

Goal state after:
case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
inst✝ : IndiscreteTopology X
v : Set X
⊢ v = ∅ ∨ v = univ → ∅.Nonempty → v.Nonempty → (∅ ∩ v).Nonempty

case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
inst✝ : IndiscreteTopology X
u v : Set X
h✝ : u = univ
⊢ v = ∅ ∨ v = univ → u.Nonempty → v.Nonempty → (u ∩ v).Nonempty
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
a b : X
hab : a ⤳ b
ha : a ∈ s
hb : b ∈ s
⊢ a = b

Tactic:
by
  let := hs.1
  simpa only [← Topology.IsInducing.subtypeVal.specializes_iff, hab, Subtype.mk.injEq,
    true_iff] using specializes_iff_eq (X := s) (x := ⟨a, ha⟩) (y := ⟨b, hb⟩)

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
⊢ (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S)) → Disjoint (𝓝[≠] x) (𝓟 S)

pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
⊢ Disjoint (𝓝[≠] x) (𝓟 S) → (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))

Tactic:
<;>

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
⊢ (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S)) → Disjoint (𝓝[≠] x) (𝓟 S)

case mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
⊢ Disjoint (𝓝[≠] x) (𝓟 S) → (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
⊢ T2Space X → T0Space X

pp: case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
⊢ T0Space X → T2Space X

Tactic:
<;>

Goal state after:
case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
⊢ T2Space X → T0Space X

case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
⊢ T0Space X → T2Space X
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
a✝ : T2Space X
⊢ T0Space X

pp: case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
a✝ : T0Space X
⊢ T2Space X

Tactic:
<;>

Goal state after:
case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
a✝ : T2Space X
⊢ T0Space X

case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
a✝ : T0Space X
⊢ T2Space X
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: case mp
ι : Type u_4
X : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), T2Space (X i)
s : Set ((i : ι) → X i)
⊢ IsCompact s → IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval i '' s)

pp: case mpr
ι : Type u_4
X : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), T2Space (X i)
s : Set ((i : ι) → X i)
⊢ (IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval i '' s)) → IsCompact s

Tactic:
<;>

Goal state after:
case mp
ι : Type u_4
X : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), T2Space (X i)
s : Set ((i : ι) → X i)
⊢ IsCompact s → IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval i '' s)

case mpr
ι : Type u_4
X : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), T2Space (X i)
s : Set ((i : ι) → X i)
⊢ (IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval i '' s)) → IsCompact s
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: case mp
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ f x ≠ g x → ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x

pp: case mpr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ (∀ᶠ (x : X) in 𝓝 x, f x ≠ g x) → f x ≠ g x

Tactic:
<;>

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ f x ≠ g x → ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x

case mpr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ (∀ᶠ (x : X) in 𝓝 x, f x ≠ g x) → f x ≠ g x
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: case mp
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst✝ : (𝓝[≠] x).NeBot
⊢ f =ᶠ[𝓝[≠] x] g → f =ᶠ[𝓝 x] g

pp: case mpr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst✝ : (𝓝[≠] x).NeBot
⊢ f =ᶠ[𝓝 x] g → f =ᶠ[𝓝[≠] x] g

Tactic:
<;>

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst✝ : (𝓝[≠] x).NeBot
⊢ f =ᶠ[𝓝[≠] x] g → f =ᶠ[𝓝 x] g

case mpr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst✝ : (𝓝[≠] x).NeBot
⊢ f =ᶠ[𝓝 x] g → f =ᶠ[𝓝[≠] x] g
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
f : X → Y
x : X
y : Y
h : Tendsto f (𝓝 x) (𝓝 y)
⊢ ContinuousAt f x

Tactic:
ContinuousAt,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
f : X → Y
x : X
y : Y
h : Tendsto f (𝓝 x) (𝓝 y)
⊢ Tendsto f (𝓝 x) (𝓝 (f x))
Module: Mathlib.Topology.Order.LeftRight

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
a : α
f : α → β
⊢ ContinuousAt f a ↔ ContinuousWithinAt f (Iio a) a ∧ ContinuousWithinAt f (Ioi a) a

Tactic:
by
  rw [continuousWithinAt_Ioi_iff_Ici, continuousWithinAt_Iio_iff_Iic,
    continuousAt_iff_continuous_left_right]

Goal state after:
Module: Mathlib.Data.Set.BoolIndicator

Goal state before:
pp: case pos
α : Type u_1
s : Set α
x : α
h : x ∈ s
⊢ x ∈ s ↔ true = true

pp: case neg
α : Type u_1
s : Set α
x : α
h : ¬x ∈ s
⊢ x ∈ s ↔ False

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
s : Set α
x : α
h : x ∈ s
⊢ x ∈ s ↔ true = true

case neg
α : Type u_1
s : Set α
x : α
h : ¬x ∈ s
⊢ x ∈ s ↔ False
Module: Mathlib.Data.Set.BoolIndicator

Goal state before:
pp: case pos
α : Type u_1
s : Set α
x : α
h : x ∈ s
⊢ ¬x ∈ s ↔ False

pp: case neg
α : Type u_1
s : Set α
x : α
h : ¬x ∈ s
⊢ ¬x ∈ s ↔ false = false

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
s : Set α
x : α
h : x ∈ s
⊢ ¬x ∈ s ↔ False

case neg
α : Type u_1
s : Set α
x : α
h : ¬x ∈ s
⊢ ¬x ∈ s ↔ false = false