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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
x : α × β
⊢ ContinuousWithinAt f univ x ↔ ContinuousWithinAt (fun x_1 ↦ f (x.1, x_1)) univ x.2

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
x : α × β
⊢ ContinuousWithinAt f univ x ↔ ContinuousWithinAt (fun x_1 ↦ f (x.1, x_1)) univ x.2
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
x : α × β
⊢ ContinuousWithinAt f univ x ↔ ContinuousWithinAt (fun x_1 ↦ f (x_1, x.2)) univ x.1

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
x : α × β
⊢ ContinuousWithinAt f univ x ↔ ContinuousWithinAt (fun x_1 ↦ f (x_1, x.2)) univ x.1
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
⊢ (∀ (a : α) (b : β), (a, b) ∈ s → ContinuousWithinAt (fun x ↦ f (a, x)) {b | (a, b) ∈ s} b) ↔
    ∀ (a : α), ∀ x ∈ {b | (a, b) ∈ s}, ContinuousWithinAt (fun x ↦ f (a, x)) {b | (a, b) ∈ s} x

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
⊢ (∀ (a : α) (b : β), (a, b) ∈ s → ContinuousWithinAt (fun x ↦ f (a, x)) {b | (a, b) ∈ s} b) ↔
    ∀ (a : α), ∀ x ∈ {b | (a, b) ∈ s}, ContinuousWithinAt (fun x ↦ f (a, x)) {b | (a, b) ∈ s} x
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
B : Set (Set α)
P : Set α → Prop
hB : IsTopologicalBasis B
basis : ∀ b ∈ B, P b
sUnion : ∀ (S : Set (Set α)), (∀ s ∈ S, P s) → P (⋃₀ S)
S : Set (Set α)
hS : S ⊆ B
hs : IsOpen[t] (⋃₀ S)
⊢ P (⋃₀ S)

Tactic:
;

Goal state after:
α : Type u
t : TopologicalSpace α
B : Set (Set α)
P : Set α → Prop
hB : IsTopologicalBasis B
basis : ∀ b ∈ B, P b
sUnion : ∀ (S : Set (Set α)), (∀ s ∈ S, P s) → P (⋃₀ S)
S : Set (Set α)
hS : S ⊆ B
hs : IsOpen[t] (⋃₀ S)
⊢ P (⋃₀ S)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
B : Set (Set α)
s t : Set α
hB : IsTopologicalBasis B
hs : IsOpen[t✝] s
h : ∀ U ∈ B, U ⊆ s → U ⊆ t
⊢ ⋃₀ {s_1 | s_1 ∈ B ∧ s_1 ⊆ s} ⊆ t

Tactic:
;

Goal state after:
α : Type u
t✝ : TopologicalSpace α
B : Set (Set α)
s t : Set α
hB : IsTopologicalBasis B
hs : IsOpen[t✝] s
h : ∀ U ∈ B, U ⊆ s → U ⊆ t
⊢ ⋃₀ {s_1 | s_1 ∈ B ∧ s_1 ⊆ s} ⊆ t
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
⊢ (∀ (a : α) (b : β), (a, b) ∈ s → ContinuousWithinAt (fun x ↦ f (x, b)) {a | (a, b) ∈ s} a) ↔
    ∀ (b : β), ∀ x ∈ {a | (a, b) ∈ s}, ContinuousWithinAt (fun x ↦ f (x, b)) {a | (a, b) ∈ s} x

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
⊢ (∀ (a : α) (b : β), (a, b) ∈ s → ContinuousWithinAt (fun x ↦ f (x, b)) {a | (a, b) ∈ s} a) ↔
    ∀ (b : β), ∀ x ∈ {a | (a, b) ∈ s}, ContinuousWithinAt (fun x ↦ f (x, b)) {a | (a, b) ∈ s} x
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
⊢ ContinuousOn f univ ↔ ∀ (a : α), ContinuousOn (fun x ↦ f (a, x)) univ

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
⊢ ContinuousOn f univ ↔ ∀ (a : α), ContinuousOn (fun x ↦ f (a, x)) univ
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
⊢ ContinuousOn f univ ↔ ∀ (b : β), ContinuousOn (fun x ↦ f (x, b)) univ

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
⊢ ContinuousOn f univ ↔ ∀ (b : β), ContinuousOn (fun x ↦ f (x, b)) univ
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
⊢ IsOpenMap f ↔ ∀ (b : β), IsOpenMap fun x ↦ f (x, b)

Tactic:
simp_rw [isOpenMap_iff_nhds_le, Prod.forall, forall_comm (α := α) (β := β), nhds_prod_eq,
    nhds_discrete, prod_pure, map_map]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
⊢ (∀ (b : β) (a : α), 𝓝 (f (a, b)) ≤ map (f ∘ fun a ↦ (a, b)) (𝓝 a)) ↔
    ∀ (b : β) (x : α), 𝓝 (f (x, b)) ≤ map (fun x ↦ f (x, b)) (𝓝 x)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
⊢ (∀ (b : β) (a : α), 𝓝 (f (a, b)) ≤ map (f ∘ fun a ↦ (a, b)) (𝓝 a)) ↔
    ∀ (b : β) (x : α), 𝓝 (f (x, b)) ≤ map (fun x ↦ f (x, b)) (𝓝 x)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
⊢ (∀ (b : β) (a : α), 𝓝 (f (a, b)) ≤ map (f ∘ fun a ↦ (a, b)) (𝓝 a)) ↔
    ∀ (b : β) (x : α), 𝓝 (f (x, b)) ≤ map (fun x ↦ f (x, b)) (𝓝 x)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
hg : IsInducing g
s : Set α
x : α
⊢ Tendsto (g ∘ f) (𝓝[s] x) (𝓝 (g (f x))) ↔ Tendsto (g ∘ f) (𝓝[s] x) (𝓝 ((g ∘ f) x))

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
hg : IsInducing g
s : Set α
x : α
⊢ Tendsto (g ∘ f) (𝓝[s] x) (𝓝 (g (f x))) ↔ Tendsto (g ∘ f) (𝓝[s] x) (𝓝 ((g ∘ f) x))
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
hi : i.Finite
hs : ∀ a ∈ i, IsOpen[T a] (s a)
⊢ IsOpen[Pi.topologicalSpace] (⋂ a ∈ i, eval a ⁻¹' s a)

Tactic:
;

Goal state after:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
hi : i.Finite
hs : ∀ a ∈ i, IsOpen[T a] (s a)
⊢ IsOpen[Pi.topologicalSpace] (⋂ a ∈ i, eval a ⁻¹' s a)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsInducing f
s : Set α
x : α
s✝ : Set β
⊢ s✝ ∈ map f (𝓝[s] x) ↔ s✝ ∈ 𝓝[f '' s] f x

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsInducing f
s : Set α
x : α
s✝ : Set β
⊢ s✝ ∈ map f (𝓝[s] x) ↔ s✝ ∈ 𝓝[f '' s] f x
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable ↑(t i)
a✝ : Nontrivial ((i : ι) → X i)
⊢ SeparableSpace ((i : ι) → X i)

Tactic:
;

Goal state after:
α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable ↑(t i)
a✝ : Nontrivial ((i : ι) → X i)
⊢ SeparableSpace ((i : ι) → X i)
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: case h
α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
⊢ accumulate s 0 ⊆ s 0

Tactic:
;

Goal state after:
case h
α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
⊢ accumulate s 0 ⊆ s 0
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
n m : ℕ
hm : accumulate s n ⊆ s m
k : ℕ
hk : s m ⊆ s k ∧ s (n + 1) ⊆ s k
⊢ accumulate s n ⊆ s k ∧ s (n + 1) ⊆ s k

Tactic:
;

Goal state after:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
n m : ℕ
hm : accumulate s n ⊆ s m
k : ℕ
hk : s m ⊆ s k ∧ s (n + 1) ⊆ s k
⊢ accumulate s n ⊆ s k ∧ s (n + 1) ⊆ s k
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
hs : ∀ a ∈ i, IsClosed[T a] (s a)
⊢ IsClosed[Pi.topologicalSpace] (⋂ a ∈ i, eval a ⁻¹' s a)

Tactic:
;

Goal state after:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
hs : ∀ a ∈ i, IsClosed[T a] (s a)
⊢ IsClosed[Pi.topologicalSpace] (⋂ a ∈ i, eval a ⁻¹' s a)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
s : (i : ι) → Set (A i)
a : (i : ι) → A i
hs : I.pi s ∈ Filter.pi fun i ↦ 𝓝 (a i)
i : ι
hi : i ∈ I
⊢ s i ∈ 𝓝 (a i)

Tactic:
;

Goal state after:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
s : (i : ι) → Set (A i)
a : (i : ι) → A i
hs : I.pi s ∈ Filter.pi fun i ↦ 𝓝 (a i)
i : ι
hi : i ∈ I
⊢ s i ∈ 𝓝 (a i)
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
f : Ultrafilter α
g : Filter α
hg : (g ⊓ ↑f).NeBot
⊢ (↑f ⊓ g).NeBot

Tactic:
inf_comm

Goal state after:
α : Type u
f : Ultrafilter α
g : Filter α
hg : (g ⊓ ↑f).NeBot
⊢ (g ⊓ ↑f).NeBot
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
h₀ : optParam (Injective id) ⋯
⊢ univ ∈ f

Tactic:
;

Goal state after:
α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
h₀ : optParam (Injective id) ⋯
⊢ univ ∈ f
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter γ
m : α → β
n : β → γ
inj₀ : Injective n
large₀ : range n ∈ f
inj₁ : Injective m
large₁ : range m ∈ f.comap inj₀ large₀
inj₂ : optParam (Injective (n ∘ m)) ⋯
⊢ n '' range m ∈ f

Tactic:
;

Goal state after:
α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter γ
m : α → β
n : β → γ
inj₀ : Injective n
large₀ : range n ∈ f
inj₁ : Injective m
large₁ : range m ∈ f.comap inj₀ large₀
inj₂ : optParam (Injective (n ∘ m)) ⋯
⊢ n '' range m ∈ f
Module: Mathlib.Topology.Ultrafilter

Goal state before:
pp: X : Type u
x : X
inst✝ : TopologicalSpace X
f : Filter X
⊢ (𝓝 x ⊓ f).NeBot ↔ (f ⊓ 𝓝 x).NeBot

Tactic:
inf_comm

Goal state after:
Module: Mathlib.Topology.Ultrafilter

Goal state before:
pp: X : Type u
α : Type u_1
x : X
inst✝ : TopologicalSpace X
F : Filter α
u : α → X
⊢ (comap u (𝓝 x) ⊓ F).NeBot ↔ (F ⊓ comap u (𝓝 x)).NeBot

Tactic:
inf_comm

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝¹ : FirstCountableTopology α
x : α
f : Filter α
inst✝ : f.IsCountablyGenerated
hx : ClusterPt x f
⊢ ∃ ψ, Tendsto ψ atTop (𝓝 x) ∧ Tendsto ψ atTop f

Tactic:
unfold ClusterPt at hx
  obtain ⟨g, hg⟩ := Filter.exists_seq_tendsto (𝓝 x ⊓ f)
  exact ⟨g, (tendsto_inf.1 hg).1, (tendsto_inf.1 hg).2⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology α
inst✝ : FirstCountableTopology β
x✝ : α × β
x : α
y : β
⊢ (𝓝 x ×ˢ 𝓝 y).IsCountablyGenerated

Tactic:
;

Goal state after:
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology α
inst✝ : FirstCountableTopology β
x✝ : α × β
x : α
y : β
⊢ (𝓝 x ×ˢ 𝓝 y).IsCountablyGenerated
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
ι : Type u_1
X : ι → Type u_2
inst✝² : Countable ι
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), FirstCountableTopology (X i)
f : (i : ι) → X i
⊢ (Filter.pi fun i ↦ 𝓝 (f i)).IsCountablyGenerated

Tactic:
;

Goal state after:
α : Type u
t : TopologicalSpace α
ι : Type u_1
X : ι → Type u_2
inst✝² : Countable ι
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), FirstCountableTopology (X i)
f : (i : ι) → X i
⊢ (Filter.pi fun i ↦ 𝓝 (f i)).IsCountablyGenerated
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
⊢ ∃ b, b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b

Tactic:
obtain ⟨b, hb₁, hb₂⟩ := @SecondCountableTopology.is_open_generated_countable α _ _
  refine ⟨_, ?_, notMem_sdiff_of_mem ?_, (isTopologicalBasis_of_subbasis hb₂).sdiff_empty⟩
  exacts [((countable_ofPred_finite_subset hb₁).image _).mono sdiff_subset, rfl]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
x : X
U : Set X
hU : IsOpen[inst✝¹] U
hx : x ∈ U
⊢ ∃ K, IsCompact K ∧ x ∈ interior K ∧ K ⊆ U

Tactic:
rcases LocallyCompactSpace.local_compact_nhds x U (hU.mem_nhds hx) with ⟨K, h1K, h2K, h3K⟩
  exact ⟨K, h3K, mem_interior_iff_mem_nhds.2 h1K, h2K⟩

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ x ∈ K (K.find x)

Tactic:
classical
  exact Nat.find_spec (K.exists_mem x)

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

Goal state before:
pp: α : Type u
β : Set α
γ : Set ↑β
a✝ val✝ : α
ha : val✝ ∈ β
h✝ : ⟨val✝, ha⟩ ∈ γ
right✝ : a✝ ∈ (fun h ↦ (fun a ↦ pure ↑a) ⟨val✝, ha⟩) h✝
⊢ a✝ ∈ β

Tactic:
;

Goal state after:
α : Type u
β : Set α
γ : Set ↑β
a✝ val✝ : α
ha : val✝ ∈ β
h✝ : ⟨val✝, ha⟩ ∈ γ
right✝ : a✝ ∈ (fun h ↦ (fun a ↦ pure ↑a) ⟨val✝, ha⟩) h✝
⊢ a✝ ∈ β
Module: Mathlib.Data.Set.Functor

Goal state before:
pp: α : Type u
β : Set α
γ : Set ↑β
a : α
w✝ : ↑β
ha : w✝ ∈ γ
right✝ : a ∈ (fun h ↦ (fun a ↦ pure ↑a) w✝) ha
⊢ ⟨a, ⋯⟩ ∈ γ

Tactic:
;

Goal state after:
α : Type u
β : Set α
γ : Set ↑β
a : α
w✝ : ↑β
ha : w✝ ∈ γ
right✝ : a ∈ (fun h ↦ (fun a ↦ pure ↑a) w✝) ha
⊢ ⟨a, ⋯⟩ ∈ γ
Module: Mathlib.Data.Set.Functor

Goal state before:
pp: α : Type u
β : Set α
γ : Set ↑β
w✝ : { x // x ∈ β }
ha : w✝ ∈ γ
⊢ ⟨↑w✝, ⋯⟩ ∈ γ

Tactic:
;

Goal state after:
α : Type u
β : Set α
γ : Set ↑β
w✝ : { x // x ∈ β }
ha : w✝ ∈ γ
⊢ ⟨↑w✝, ⋯⟩ ∈ γ
Module: Mathlib.Data.Set.Functor

Goal state before:
pp: α : Type u
β : Set α
γ : Set ↑β
δ : Type u_1
f : α → δ
x✝ : δ
⊢ x✝ ∈ f '' Subtype.val '' γ ↔ x✝ ∈ β.domRestrict f '' γ

Tactic:
;

Goal state after:
α : Type u
β : Set α
γ : Set ↑β
δ : Type u_1
f : α → δ
x✝ : δ
⊢ x✝ ∈ f '' Subtype.val '' γ ↔ x✝ ∈ β.domRestrict f '' γ
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hf : S.Finite
hc : ∀ s ∈ S, IsCompact s
⊢ IsCompact (⋃ i ∈ S, i)

Tactic:
;

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hf : S.Finite
hc : ∀ s ∈ S, IsCompact s
⊢ IsCompact (⋃ i ∈ S, i)
Module: Mathlib.Topology.Compactness.Compact

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

Tactic:
;

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (⋃ b, bif b then s else t)
Module: Mathlib.Order.UpperLower.Fibration

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : LE α
inst✝ : LE β
hf : Fibration (fun x1 x2 ↦ x1 ≤ x2) (fun x1 x2 ↦ x1 ≤ x2) f
s : Set α
hs : IsLowerSet s
y' : β
x : α
hx : x ∈ s
e : y' ≤ f x
⊢ y' ∈ f '' s

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : LE α
inst✝ : LE β
hf : Fibration (fun x1 x2 ↦ x1 ≤ x2) (fun x1 x2 ↦ x1 ≤ x2) f
s : Set α
hs : IsLowerSet s
y' : β
x : α
hx : x ∈ s
e : y' ≤ f x
⊢ y' ∈ f '' s
Module: Mathlib.Order.UpperLower.Fibration

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : LE α
inst✝ : LE β
hf : Fibration (fun x1 x2 ↦ x1 ≤ x2) (fun x1 x2 ↦ x1 ≤ x2) f
s : Set α
hs : IsLowerSet s
x : α
hx : x ∈ s
y : α
e' : y ≤ x
e : f y ≤ f x
⊢ f y ∈ f '' s

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : LE α
inst✝ : LE β
hf : Fibration (fun x1 x2 ↦ x1 ≤ x2) (fun x1 x2 ↦ x1 ≤ x2) f
s : Set α
hs : IsLowerSet s
x : α
hx : x ∈ s
y : α
e' : y ≤ x
e : f y ≤ f x
⊢ f y ∈ f '' s
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ s ⊆ ↑⊤ ↔ s = ∅

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ s ⊆ ↑⊤ ↔ s = ∅
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
⊢ s.sdiff {a} = s ↔ a ∉ s

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
⊢ s.sdiff {a} = s ↔ a ∉ s
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
⊢ s.erase a = s ↔ a ∉ s

Tactic:
by rw [← sdiff_singleton]; simp [-sdiff_singleton]

Goal state after:
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
t : UpperSet α
carrier✝ : Set α
upper'✝ : IsUpperSet carrier✝
h : { carrier := carrier✝, upper' := upper'✝ }.carrier = t.carrier
⊢ { carrier := carrier✝, upper' := upper'✝ } = t

Tactic:
;

Goal state after:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
t : UpperSet α
carrier✝ : Set α
upper'✝ : IsUpperSet carrier✝
h : { carrier := carrier✝, upper' := upper'✝ }.carrier = t.carrier
⊢ { carrier := carrier✝, upper' := upper'✝ } = t
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
carrier✝¹ : Set α
upper'✝¹ : IsUpperSet carrier✝¹
carrier✝ : Set α
upper'✝ : IsUpperSet carrier✝
h : { carrier := carrier✝¹, upper' := upper'✝¹ }.carrier = { carrier := carrier✝, upper' := upper'✝ }.carrier
⊢ { carrier := carrier✝¹, upper' := upper'✝¹ } = { carrier := carrier✝, upper' := upper'✝ }

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
carrier✝¹ : Set α
upper'✝¹ : IsUpperSet carrier✝¹
carrier✝ : Set α
upper'✝ : IsUpperSet carrier✝
h : { carrier := carrier✝¹, upper' := upper'✝¹ }.carrier = { carrier := carrier✝, upper' := upper'✝ }.carrier
⊢ { carrier := carrier✝¹, upper' := upper'✝¹ } = { carrier := carrier✝, upper' := upper'✝ }
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
⊢ upperClosure t ⊓ s.sdiff t = s

Tactic:
inf_comm,

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
⊢ s.sdiff t ⊓ upperClosure t = s
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
f : ι → X
x : X
hf : Tendsto f cofinite (𝓝 x)
this : TopologicalSpace ι := ⊥
⊢ IsCompact (insert x (range f))

Tactic:
;

Goal state after:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
f : ι → X
x : X
hf : Tendsto f cofinite (𝓝 x)
this : TopologicalSpace ι := ⊥
⊢ IsCompact (insert x (range f))
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ Ici a ⊓ s.erase a = s

Tactic:
inf_comm,

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ s.erase a ⊓ Ici a = s
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x✝¹ : UpperSet β
x✝ : α
⊢ x✝ ∈ ↑((map f).symm x✝¹) ↔ x✝ ∈ ↑((map f.symm) x✝¹)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x✝¹ : UpperSet β
x✝ : α
⊢ x✝ ∈ ↑((map f).symm x✝¹) ↔ x✝ ∈ ↑((map f.symm) x✝¹)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
ι : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
f : X → Y
inst✝ : NoncompactSpace X
i✝ : Set X
hs : ¬i✝ᶜ.Nonempty
⊢ ¬IsCompact i✝

Tactic:
;

Goal state after:
X : Type u
Y : Type v
ι : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
f : X → Y
inst✝ : NoncompactSpace X
i✝ : Set X
hs : ¬i✝ᶜ.Nonempty
⊢ ¬IsCompact i✝
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
ι : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
f : X → Y
inst✝ : NoncompactSpace X
i✝ : Set X
hs : i✝ = univ
⊢ ¬IsCompact univ

Tactic:
;

Goal state after:
X : Type u
Y : Type v
ι : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
f : X → Y
inst✝ : NoncompactSpace X
i✝ : Set X
hs : i✝ = univ
⊢ ¬IsCompact univ
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s K : Set X
hs : s.Infinite
hK : IsCompact K
hsub : s ⊆ K
x : X
hx : x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s)
⊢ x ∈ K ∧ ClusterPt x (𝓟 {x}ᶜ ⊓ (cofinite ⊓ 𝓟 s))

Tactic:
inf_comm,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s K : Set X
hs : s.Infinite
hK : IsCompact K
hsub : s ⊆ K
x : X
hx : x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s)
⊢ x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s ⊓ 𝓟 {x}ᶜ)
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x x✝ : X
⊢ x✝ ∈ (𝓝 x).ker ↔ x✝ ∈ {y | y ⤳ x}

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x x✝ : X
⊢ x✝ ∈ (𝓝 x).ker ↔ x✝ ∈ {y | y ⤳ x}
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ IsCompact (f '' univ)

Tactic:
;

Goal state after:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ IsCompact (f '' univ)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
inst✝ : CompactSpace X
hf' : Surjective f
⊢ IsCompact univ

Tactic:
rw [← hf'.range_eq]
    exact isCompact_range hf

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : CompactSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsCompact (range f)

Tactic:
;

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : CompactSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsCompact (range f)