mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Filter β
m : β → γ
hg : Monotone g
this : Monotone (map m ∘ g)
s : Set γ
⊢ s ∈ map m (f.lift g) ↔ s ∈ f.lift (map m ∘ g)

Tactic:
simp only [mem_lift_sets hg, mem_lift_sets this, mem_map, Function.comp_apply]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ ⋂₀ {t | IsClosed t ∧ s ⊆ t} = ⋂₀ {s_1 | IsOpen s_1ᶜ ∧ s_1ᶜ ⊆ sᶜ}

Tactic:
simp only [compl_subset_compl, isOpen_compl_iff]

Goal state after:
Module: Mathlib.Topology.Defs.Induced

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
S : Set (Set X)
g : Set X → Set Y
hgo : ∀ t_1 ∈ S, IsOpen[t] (g t_1)
hfg : ∀ t ∈ S, f ⁻¹' g t = t
⊢ ∃ t_1, IsOpen[t] t_1 ∧ f ⁻¹' t_1 = ⋃₀ S

Tactic:
refine ⟨⋃₀ (g '' S), isOpen_sUnion <| forall_mem_image.2 hgo, ?_⟩

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
S : Set (Set X)
g : Set X → Set Y
hgo : ∀ t_1 ∈ S, IsOpen[t] (g t_1)
hfg : ∀ t ∈ S, f ⁻¹' g t = t
⊢ f ⁻¹' ⋃₀ (g '' S) = ⋃₀ S
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b c : α
n : ℤ
a z✝ : α
⊢ (fun x ↦ ↑↑x) ((fun b ↦ ⟨⋯.lift b, ⋯⟩) ↑z✝) = ↑z✝

Tactic:
dsimp

Goal state after:
case H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b c : α
n : ℤ
a z✝ : α
⊢ ↑(toIcoMod hp a z✝) = ↑z✝
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b c : α
n : ℤ
a z✝ : α
⊢ (fun x ↦ ↑↑x) ((fun b ↦ ⟨⋯.lift b, ⋯⟩) ↑z✝) = ↑z✝

Tactic:
dsimp

Goal state after:
case H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b c : α
n : ℤ
a z✝ : α
⊢ ↑(toIocMod hp a z✝) = ↑z✝
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a b = a + Int.fract ((b - a) / p) * p

Tactic:
rw [toIcoMod, toIcoDiv_eq_floor, Int.fract]
  simp [field, -Int.self_sub_floor]
  ring

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
t : TopologicalSpace α
b : Set (Set β)
⊢ Continuous[t, generateFrom b] f ↔ ∀ s ∈ b, IsOpen[t] (f ⁻¹' s)

Tactic:
continuous_iff_coinduced_le,

Goal state after:
α : Type u
β : Type v
f : α → β
t : TopologicalSpace α
b : Set (Set β)
⊢ coinduced f t ≤ generateFrom b ↔ ∀ s ∈ b, IsOpen[t] (f ⁻¹' s)
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : IsQuotientMap f
⊢ Continuous[inst✝¹, inst✝] g ↔ Continuous[inst✝², inst✝] (g ∘ f)

Tactic:
continuous_iff_coinduced_le,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : IsQuotientMap f
⊢ coinduced g inst✝¹ ≤ inst✝ ↔ Continuous[inst✝², inst✝] (g ∘ f)
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : IsQuotientMap f
⊢ coinduced g inst✝¹ ≤ inst✝ ↔ Continuous[inst✝², inst✝] (g ∘ f)

Tactic:
continuous_iff_coinduced_le,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : IsQuotientMap f
⊢ coinduced g inst✝¹ ≤ inst✝ ↔ coinduced (g ∘ f) inst✝² ≤ inst✝
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
h : s ∈ 𝓝[t] a
⊢ 𝓝[t] a ≤ 𝓝[s] a

Tactic:
exact nhdsWithin_le_of_mem h

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) s t)
v : Set Y
hv : v ∈ t
⊢ ⋃ u ∈ s, u ×ˢ v = Prod.snd ⁻¹' v

Tactic:
← iUnion_prod_const,

Goal state after:
X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) s t)
v : Set Y
hv : v ∈ t
⊢ (⋃ i ∈ s, i) ×ˢ v = Prod.snd ⁻¹' v
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set α
l : Filter β
h : Tendsto f l (𝓝[s] a)
⊢ ∀ᶠ (i : β) in l, f i ∈ s

Tactic:
nhdsWithin_eq,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set α
l : Filter β
h : Tendsto f l (⨅ t ∈ {t | a ∈ t ∧ IsOpen[inst✝] t}, 𝓟 (t ∩ s))
⊢ ∀ᶠ (i : β) in l, f i ∈ s
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : Dense s
u : Set ↑s
hud : Dense u
v : Set X
hv1 : IsOpen[inst✝] v
hv2 : Subtype.val ⁻¹' v = u
⊢ ∃ v, IsOpen[inst✝] v ∧ Dense v ∧ Subtype.val ⁻¹' v = u

Tactic:
refine ⟨v, hv1, ?_, hv2⟩

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : Dense s
u : Set ↑s
hud : Dense u
v : Set X
hv1 : IsOpen[inst✝] v
hv2 : Subtype.val ⁻¹' v = u
⊢ Dense v
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
B B' : Set (Set α)
hB : IsTopologicalBasis B
h_open : ∀ u ∈ B', IsOpen[t] u
h : ∀ u ∈ B, ∀ x ∈ u, ∃ v ∈ B', x ∈ v ∧ v ⊆ u
⊢ IsTopologicalBasis B'

Tactic:
by
  refine isTopologicalBasis_of_isOpen_of_nhds h_open fun x u hx hu => ?_
  obtain ⟨w, hwB, hxw, hwu⟩ := hB.exists_subset_of_mem_open hx hu
  obtain ⟨v, hvB', hxv, hvw⟩ := h w hwB x hxw
  exact ⟨v, hvB', hxv, hvw.trans hwu⟩

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case e'_3
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : Y
⊢ (range f)ᶜ ∈ 𝓝 (g x)

Tactic:
rw [← disjoint_principal_left]

Goal state after:
case e'_3
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : Y
⊢ Disjoint (𝓟 (range f)) (𝓝 (g x))
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
h : IsInducing (Sum.elim f g)
⊢ Disjoint (closure[inst✝] (range f)) (range g)

Tactic:
rcases h.isClosed_iff.mp isClosed_range_inl with ⟨C, C_closed, hC⟩

Goal state after:
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst✝] C
hC : Sum.elim f g ⁻¹' C = range inl
⊢ Disjoint (closure[inst✝] (range f)) (range g)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: Y : Type v
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : DecidableEq ι
l : Filter Y
f : Y → (i : ι) → A i
x : (i : ι) → A i
hf : Tendsto f l (𝓝 x)
i : ι
g : Y → A i
xi : A i
hg : Tendsto g l (𝓝 xi)
j : ι
⊢ Tendsto (fun i_1 ↦ Function.update (f i_1) i (g i_1) j) l (𝓝 (Function.update x i xi j))

Tactic:
rcases eq_or_ne j i with (rfl | hj) <;> simp [*, hf.apply_nhds]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : Finite ι
s : Set ((a : ι) → A a)
val✝ : Fintype ι
a : (a : ι) → A a
x✝¹ : a ∈ s
x✝ : ∃ u, (∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ univ.pi u ⊆ s
u : (a : ι) → Set (A a)
h1 : ∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1
right✝ : univ.pi u ⊆ s
⊢ (↑Finset.univ).pi u ⊆ s

Tactic:
by rwa [Finset.coe_univ]

Goal state after:
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)
x : (a : ι) → A a
hi : i.Finite
hs : ∀ a ∈ i, s a ∈ 𝓝 (x a)
⊢ ∀ i_1 ∈ i, eval i_1 ⁻¹' s i_1 ∈ 𝓝 x

Tactic:
exact fun a ha => (continuous_apply a).continuousAt (hs a ha)

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t

Tactic:
rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, htd⟩

Goal state after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h_open
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : Set α → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
⊢ ∀ (u x : Set α), x ∈ countableBasis α → u ∈ s x → IsOpen[t✝] u

Tactic:
have := @ht.isOpen

Goal state after:
case h_open
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : Set α → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
this : ∀ s ∈ t, IsOpen[t✝] s
⊢ ∀ (u x : Set α), x ∈ countableBasis α → u ∈ s x → IsOpen[t✝] u
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsClosed[inst✝] s
h : s ⊆ t
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcov : ⋃ n, K n = t
⊢ ⋃ n, (fun n ↦ s ∩ K n) n = s

Tactic:
← inter_iUnion,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsClosed[inst✝] s
h : s ⊆ t
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcov : ⋃ n, K n = t
⊢ s ∩ ⋃ i, K i = s
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : SigmaCompactSpace X
e : Y → X
he : IsClosedEmbedding e
⊢ e ⁻¹' ⋃ i, compactCovering X i = univ

Tactic:
iUnion_compactCovering,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : SigmaCompactSpace X
e : Y → X
he : IsClosedEmbedding e
⊢ e ⁻¹' univ = univ
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
⊢ ∃ n, s ⊆ K n

Tactic:
by
  suffices ∃ n, s ⊆ interior (K n) from this.imp fun _ ↦ (Subset.trans · interior_subset)
  refine hs.elim_directed_cover (interior ∘ K) (fun _ ↦ isOpen_interior) ?_ ?_
  · intro x _
    rcases K.exists_mem x with ⟨k, hk⟩
    exact mem_iUnion.2 ⟨k + 1, K.subset_interior_succ _ hk⟩
  · exact Monotone.directed_le fun _ _ h ↦ interior_mono <| K.subset h

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

Goal state before:
pp: α : Type u
β : Set α
γ : Set ↑β
a : α
ha : a ∈ Subtype.val '' γ
⊢ ⟨a, ⋯⟩ ∈ γ

Tactic:
by
  rcases ha with ⟨_, ha, rfl⟩; exact ha

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

Tactic:
simp only [and_imp, mem_inter_iff, mem_compl_iff]

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
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
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:
simp only [and_imp, mem_inter_iff, mem_compl_iff]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ (x ~ᵢ y) ↔ closure[inst✝] {x} = closure[inst✝] {y}

Tactic:
by
  simp only [inseparable_iff_specializes_and, specializes_iff_closure_subset, ← subset_antisymm_iff,
    eq_comm]

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
f : X → Y
hf : IsInducing f
⊢ (f x ~ᵢ f y) ↔ (x ~ᵢ y)

Tactic:
simp only [inseparable_iff_specializes_and, hf.specializes_iff]

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

Goal state before:
pp: case mp
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s K : Set ((i : ι) → X i)
hK : IsCompact K
hsK : s ⊆ K
i : ι
⊢ ∃ Ki, IsCompact Ki ∧ s ⊆ eval i ⁻¹' Ki

Tactic:
exact ⟨eval i '' K, hK.image <| continuous_apply i, hsK.trans <| K.subset_preimage_image _⟩

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: 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
⊢ IsOpen[inst✝²] u → IsOpen[inst✝²] v → (univ ∩ u).Nonempty → (univ ∩ v).Nonempty → (univ ∩ (u ∩ v)).Nonempty

Tactic:
simp only [IndiscreteTopology.isOpen_iff, univ_inter]

Goal state after:
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
⊢ u = ∅ ∨ u = univ → v = ∅ ∨ v = univ → u.Nonempty → v.Nonempty → (u ∩ v).Nonempty
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst✝] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst✝] {x}) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
⊢ (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ

Tactic:
refine forall_comm.trans ?_

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst✝] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst✝] {x}) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
⊢ (∀ (b a : X), a ≠ b → {b}ᶜ ∈ 𝓝 a) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
Module: Mathlib.Order.SuccPred.Relation

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
⊢ (∀ i ∈ Ico n n, r i (succ i)) → ReflTransGen r n n

pp: case refine_2
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
⊢ ∀ (n_1 : α),
    n ≤ n_1 →
      ((∀ i ∈ Ico n n_1, r i (succ i)) → ReflTransGen r n n_1) →
        (∀ i ∈ Ico n (succ n_1), r i (succ i)) → ReflTransGen r n (succ n_1)

Tactic:
· intro _
    exact ReflTransGen.refl

Goal state after:
case refine_2
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
⊢ ∀ (n_1 : α),
    n ≤ n_1 →
      ((∀ i ∈ Ico n n_1, r i (succ i)) → ReflTransGen r n n_1) →
        (∀ i ∈ Ico n (succ n_1), r i (succ i)) → ReflTransGen r n (succ n_1)
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
t : Set X
ht : t.Finite
⊢ Dense (s \ t)

Tactic:
by
  convert! hs.sdiff_finset ht.toFinset
  exact (Finite.coe_toFinset _).symm

Goal state after:
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
⊢ Disjoint (𝓝 a) atBot ↔ ¬IsBot a

Tactic:
constructor
  · intro hd hbot
    rw [hbot.atBot_eq, disjoint_principal_right] at hd
    exact mem_of_mem_nhds hd le_rfl
  · simp only [IsBot, not_forall]
    rintro ⟨b, hb⟩
    refine disjoint_of_disjoint_of_mem disjoint_compl_left ?_ (Iic_mem_atBot b)
    exact isClosed_Iic.isOpen_compl.mem_nhds hb

Goal state after:
Module: Mathlib.Topology.Clopen

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : Disjoint a b
this : IsClosed[inst✝] (s ∩ bᶜ)
x : X
hx₁ : x ∈ s
hx₂ : x ∈ bᶜ
⊢ x ∈ a

Tactic:
by simpa [notMem_of_mem_compl hx₂] using cover hx₁

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : ∀ x ∈ s, ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
⊢ IsPreconnected s

Tactic:
rcases eq_empty_or_nonempty s with (rfl | ⟨x, hx⟩)

Goal state after:
case inl
α : Type u
inst✝ : TopologicalSpace α
H : ∀ x ∈ ∅, ∀ y ∈ ∅, ∃ t ⊆ ∅, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
⊢ IsPreconnected ∅

case inr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : ∀ x ∈ s, ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
x : α
hx : x ∈ s
⊢ IsPreconnected s
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst✝², inst✝¹] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
⊢ ∃ L ∈ 𝓝 x, IsCompact L ∧ MapsTo f L s

Tactic:
have hc : IsCompact (f '' K \ interior s) := (hKc.image hf).diff isOpen_interior
  obtain ⟨U, V, Uo, Vo, hxU, hV, hd⟩ : SeparatedNhds {f x} (f '' K \ interior s) := by
    simp_rw [separatedNhds_iff_disjoint, nhdsSet_singleton, hc.disjoint_nhdsSet_right,
      disjoint_nhds_nhds_iff_not_inseparable]
    rintro y ⟨-, hys⟩ hxy
    refine hys <| (hxy.mem_open_iff isOpen_interior).1 ?_
    rwa [mem_interior_iff_mem_nhds]
  refine ⟨K \ f ⁻¹' V, sdiff_mem hKx ?_, hKc.diff <| Vo.preimage hf, fun y hy ↦ ?_⟩
  · filter_upwards [hf.continuousAt <| Uo.mem_nhds (hxU rfl)] with x hx
      using Set.disjoint_left.1 hd hx
  · by_contra hys
    exact hy.2 (hV ⟨mem_image_of_mem _ hy.1, notMem_subset interior_subset hys⟩)

Goal state after:
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝¹ : CountableInterFilter l✝
l : Filter α
inst✝ : CountableInterFilter l
f : α → β
S : Set (Set β)
hSc : S.Countable
hS : ∀ s ∈ S, f ⁻¹' s ∈ l
⊢ ⋂ i ∈ S, f ⁻¹' i ∈ l

Tactic:
exact (countable_bInter_mem hSc).2 hS

Goal state after:
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x
tfae_5_to_6 : (∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x) → ∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x
tfae_6_to_4 : (∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x) → ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst✝] t ∧ t ⊆ s
H : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst✝] t ∧ t ⊆ s
s : Set X
a : X
ha : a ∉ closure[inst✝] s
ha' : sᶜ ∈ 𝓝 a
U : Set X
hU : U ∈ 𝓝 a
hUc : IsClosed[inst✝] U
hUs : U ⊆ sᶜ
⊢ s ⊆ interior Uᶜ

Tactic:
hUc.isOpen_compl.interior_eq,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x
tfae_5_to_6 : (∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x) → ∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x
tfae_6_to_4 : (∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x) → ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst✝] t ∧ t ⊆ s
H : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst✝] t ∧ t ⊆ s
s : Set X
a : X
ha : a ∉ closure[inst✝] s
ha' : sᶜ ∈ 𝓝 a
U : Set X
hU : U ∈ 𝓝 a
hUc : IsClosed[inst✝] U
hUs : U ⊆ sᶜ
⊢ s ⊆ Uᶜ
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hss : s ⊆ u ∪ v
huv : Disjoint u v
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
apply H u v hu hv hss

Goal state after:
case refine_1
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hss : s ⊆ u ∪ v
huv : Disjoint u v
⊢ s ∩ (u ∩ v) = ∅
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
⊢ (connectedComponentIn F x).Nonempty ↔ x ∈ F

Tactic:
connectedComponentIn

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
⊢ (if h : x ∈ F then Subtype.val '' connectedComponent ⟨x, h⟩ else ∅).Nonempty ↔ x ∈ F
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
F : Set α
x : α
⊢ connectedComponentIn F x ⊆ F

Tactic:
connectedComponentIn

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
F : Set α
x : α
⊢ (if h : x ∈ F then Subtype.val '' connectedComponent ⟨x, h⟩ else ∅) ⊆ F
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
⊢ IsPreconnected (connectedComponentIn F x)

Tactic:
connectedComponentIn

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
⊢ IsPreconnected (if h : x ∈ F then Subtype.val '' connectedComponent ⟨x, h⟩ else ∅)
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
s : Set α
a : α
di : IsDenseInducing i
hs : s ∈ 𝓝 a
⊢ closure[inst✝] (i '' s) ∈ 𝓝 (i a)

Tactic:
rw [di.nhds_eq_comap a, ((nhds_basis_opens _).comap _).mem_iff] at hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
s : Set α
a : α
di : IsDenseInducing i
hs : ∃ i_1, (i a ∈ i_1 ∧ IsOpen[inst✝] i_1) ∧ i ⁻¹' i_1 ⊆ s
⊢ closure[inst✝] (i '' s) ∈ 𝓝 (i a)