mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ b - toIocMod hp a b = toIocDiv hp a b • p

Tactic:
by
  rw [toIocMod, sub_sub_cancel]

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
α : Type u_1
s : Set X
inst✝ : TopologicalSpace X
f : α → Set X
ho : ∀ (i : α), IsOpen[inst✝] (f i)
hU : ⋃ i, f i = univ
h : ∀ (i : α), IsOpen[inst✝] (f i ∩ s)
⊢ IsOpen[inst✝] s

Tactic:
rw [← s.inter_univ, inter_comm, ← hU, iUnion_inter]

Goal state after:
X : Type u
α : Type u_1
s : Set X
inst✝ : TopologicalSpace X
f : α → Set X
ho : ∀ (i : α), IsOpen[inst✝] (f i)
hU : ⋃ i, f i = univ
h : ∀ (i : α), IsOpen[inst✝] (f i ∩ s)
⊢ IsOpen[inst✝] (⋃ i, f i ∩ s)
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
⊢ s ∈ (iInf f).lift g → s ∈ ⨅ i, (f i).lift g

Tactic:
have H : ∀ t ∈ iInf f, ⨅ i, (f i).lift g ≤ g t := by
    intro t ht
    refine iInf_sets_induct ht ?_ fun hs ht => ?_
    · inhabit ι
      exact iInf₂_le_of_le default univ (iInf_le _ univ_mem)
    · rw [hg]
      exact le_inf (iInf₂_le_of_le _ _ <| iInf_le _ hs) ht

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
H : ∀ t ∈ iInf f, ⨅ i, (f i).lift g ≤ g t
⊢ s ∈ (iInf f).lift g → s ∈ ⨅ i, (f i).lift g
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure s = (interior sᶜ)ᶜ

Tactic:
rw [interior, closure, compl_sUnion, compl_image_ofPred]
  simp only [compl_subset_compl, isOpen_compl_iff]

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s U : Set X
h : U ∈ ⨆ x ∈ s, 𝓝 x
⊢ ∀ x ∈ s, U ∈ 𝓝 x

Tactic:
by simpa using h

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
h : pure x ≤ F.lift' closure[inst✝]
⊢ (pure x ⊓ F.lift' closure[inst✝]).NeBot

Tactic:
simp [h, pure_neBot]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace α
s : Set β
f : α → β
⊢ IsClosed[TopologicalSpace.coinduced f t] s ↔ IsClosed[t] (f ⁻¹' s)

Tactic:
simp only [← isOpen_compl_iff, isOpen_coinduced (f := f), preimage_compl]

Goal state after:
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 Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hg : IsInducing g
⊢ Continuous[inst✝¹, inst✝²] f ↔ Continuous[inst✝¹, inst✝] (g ∘ f)

Tactic:
continuous_iff_continuousAt,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hg : IsInducing g
⊢ (∀ (x : X), ContinuousAt f x) ↔ ∀ (x : X), ContinuousAt (g ∘ f) x
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
⊢ Continuous[t₁ ⊔ t₂, t₃] f ↔ Continuous[t₁, t₃] f ∧ Continuous[t₂, t₃] f

Tactic:
by
  simp only [continuous_iff_le_induced, sup_le_iff]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
W : Type u_3
Z✝ : Type u_4
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X ≃ Y
hf : IsInducing ⇑f
⊢ Continuous[inst✝¹, inst✝¹] (⇑f ∘ f.invFun)

Tactic:
by simpa using continuous_id

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

Goal state before:
pp: X : Type u_5
Y : Type u_6
Z : Type u_7
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X → Y
he : IsHomeomorph e
f : Y → Z
s : Set Z
⊢ f ∘ e '' interior (f ∘ e ⁻¹' s) = f '' interior (f ⁻¹' s)

Tactic:
simp only [Set.preimage_comp, Set.image_comp, he.image_interior,
    Set.image_preimage_eq _ he.surjective]

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

Goal state before:
pp: Y : Type v
Z : Type u_2
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
X : Type u_5
seq : X → Y × Z
f : Filter X
p : Y × Z
⊢ Tendsto seq f (𝓝 p.1 ×ˢ 𝓝 p.2) ↔ Tendsto (fun n ↦ (seq n).1) f (𝓝 p.1) ∧ Tendsto (fun n ↦ (seq n).2) f (𝓝 p.2)

Tactic:
Filter.tendsto_prod_iff'

Goal state after:
Y : Type v
Z : Type u_2
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
X : Type u_5
seq : X → Y × Z
f : Filter X
p : Y × Z
⊢ Tendsto (fun n ↦ (seq n).1) f (𝓝 p.1) ∧ Tendsto (fun n ↦ (seq n).2) f (𝓝 p.2) ↔
    Tendsto (fun n ↦ (seq n).1) f (𝓝 p.1) ∧ Tendsto (fun n ↦ (seq n).2) f (𝓝 p.2)
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ 𝓝[insert a s] a = pure a ⊔ 𝓝[s] a

Tactic:
← singleton_union,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ 𝓝[{a} ∪ s] a = pure a ⊔ 𝓝[s] a
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s u : Set α
t v : Set β
a : α
b : β
hu : u ∈ 𝓝[s] a
hv : v ∈ 𝓝[t] b
⊢ u ×ˢ v ∈ 𝓝[s ×ˢ t] (a, b)

Tactic:
by
  rw [nhdsWithin_prod_eq]
  exact prod_mem_prod hu hv

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsOpen[instTopologicalSpaceSum] (range inl)ᶜ

Tactic:
compl_range_inl

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsOpen[instTopologicalSpaceSum] (range inr)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : t.Countable ∧ ∅ ∉ t ∧ IsTopologicalBasis t
hn : t = ∅
⊢ IsTopologicalBasis (range fun n ↦ ∅)

Tactic:
by simp_all

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
ι : Sort u_2
inst✝ : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), SecondCountableTopology α
⊢ SecondCountableTopology α

Tactic:
← generateFrom_iUnion

Goal state after:
α : Type u_1
ι : Sort u_2
inst✝ : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), SecondCountableTopology α
⊢ SecondCountableTopology α
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: case refine_3
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s✝ t✝ : Set X✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
⊢ IsCompact (s.pi n'')

Tactic:
· classical
      rw [← Set.univ_pi_ite]
      refine isCompact_univ_pi fun i => ?_
      by_cases h : i ∈ s
      · rw [if_pos h]
        exact hc i
      · rw [if_neg h]
        exact CompactSpace.isCompact_univ

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

Goal state before:
pp: case inr
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
hι : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsCompact (s i)
h✝ : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
⊢ IsSigmaCompact (⋃ i, s i)

Tactic:
exact ⟨s ∘ f, fun n ↦ hcomp (f n), Function.Surjective.iUnion_comp hf _⟩

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

Goal state before:
pp: case refine_2
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen[inst✝] (c ↑x)
hc₂ : s ⊆ ⋃ x, c ↑x
d : Finset ↑b
hd : s ⊆ ⋃ i ∈ d, c ↑i
⊢ s ⊆ ⋃ i ∈ Subtype.val '' ↑d, c i

Tactic:
· rwa [biUnion_image]

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

Goal state before:
pp: case refine_1
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ i, (IsClosed[inst✝] i ∧ IsCompact i) ∧ iᶜ ⊆ s) → IsCompact (closure[inst✝] sᶜ)

pp: case refine_2
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsCompact (closure[inst✝] sᶜ)
⊢ ∃ i, (IsClosed[inst✝] i ∧ IsCompact i) ∧ iᶜ ⊆ s

Tactic:
· rintro ⟨t, ⟨htcl, htco⟩, hst⟩
    exact htco.of_isClosed_subset isClosed_closure <|
      closure_minimal (compl_subset_comm.2 hst) htcl

Goal state after:
case refine_2
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsCompact (closure[inst✝] sᶜ)
⊢ ∃ i, (IsClosed[inst✝] i ∧ IsCompact i) ∧ iᶜ ⊆ s
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx : x ∈ s
hx' : x ∈ frontier {a | p a}
⊢ ContinuousWithinAt (fun a ↦ if p a then f a else g a) s x

pp: case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx : x ∈ s
hx' : x ∉ frontier {a | p a}
⊢ ContinuousWithinAt (fun a ↦ if p a then f a else g a) s x

Tactic:
· exact (hpf x ⟨hx, hx'⟩).piecewise_nhdsWithin (hpg x ⟨hx, hx'⟩)

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx : x ∈ s
hx' : x ∉ frontier {a | p a}
⊢ ContinuousWithinAt (fun a ↦ if p a then f a else g a) s x
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed[inst✝] (t i)) → ⋂ i, t i = ∅ → ∃ u, ⋂ i ∈ u, t i = ∅
ι✝ : Type u
t : ι✝ → Set X
⊢ (∀ (i : ι✝), IsClosed[inst✝] (t i)) → univ ∩ ⋂ i, t i = ∅ → ∃ u, univ ∩ ⋂ i ∈ u, t i = ∅

Tactic:
simpa using h t

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
⊢ ContinuousOn (fun a ↦ if p a then f a else g a) s

Tactic:
by
  intro x hx
  by_cases hx' : x ∈ frontier { a | p a }
  · exact (hpf x ⟨hx, hx'⟩).piecewise_nhdsWithin (hpg x ⟨hx, hx'⟩)
  · rw [← inter_univ s, ← union_compl_self { a | p a }, inter_union_distrib_left] at hx ⊢
    rcases hx with hx | hx
    · apply ContinuousWithinAt.union
      · exact (hf x hx).congr (fun y hy => if_pos hy.2) (if_pos hx.2)
      · have : x ∉ closure { a | p a }ᶜ := fun h => hx' ⟨subset_closure hx.2, by
          rwa [closure_compl] at h⟩
        exact continuousWithinAt_of_notMem_closure fun h =>
          this (closure_inter_subset_inter_closure _ _ h).2
    · apply ContinuousWithinAt.union
      · have : x ∉ closure { a | p a } := fun h =>
          hx' ⟨h, fun h' : x ∈ interior { a | p a } => hx.2 (interior_subset h')⟩
        exact continuousWithinAt_of_notMem_closure fun h =>
          this (closure_inter_subset_inter_closure _ _ h).2
      · exact (hg x hx).congr (fun y hy => if_neg hy.2) (if_neg hx.2)

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ ⦃U V : Set X⦄, IsOpen[inst✝] U → IsOpen[inst✝] V → U.Nonempty → V.Nonempty → (U ∩ V).Nonempty
x✝ : Set X
⊢ ∀ (v : Set X),
    IsOpen[inst✝] x✝ → IsOpen[inst✝] v → (univ ∩ x✝).Nonempty → (univ ∩ v).Nonempty → (univ ∩ (x✝ ∩ v)).Nonempty

Tactic:
by simp_all

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : PreirreducibleSpace ↑s
⊢ IsPreirreducible (range Subtype.val)

Tactic:
← Set.image_univ

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : PreirreducibleSpace ↑s
⊢ IsPreirreducible (Subtype.val '' univ)
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S T : Set X
⊢ S ∈ codiscreteWithin T ↔ ∀ x ∈ T, Disjoint (𝓝[≠] x) (𝓟 (T \ S))

Tactic:
simp only [codiscreteWithin, mem_iSup, mem_nhdsWithin, disjoint_principal_right, subset_def,
    Set.mem_sdiff, mem_inter_iff, mem_compl_iff]
  congr! 7 with x - u y
  tauto

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

Goal state before:
pp: case inr
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x✝¹ : X × X
x y : X
x✝ : (x, y) ∈ s ×ˢ s
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
hne : x ≠ y
⊢ ∀ᶠ (y : X × X) in 𝓝 (x, y), f y.1 = f y.2 → y.1 = y.2

Tactic:
· suffices ∀ᶠ z in 𝓝 (x, y), f z.1 ≠ f z.2 from this.mono fun _ hne h ↦ absurd h hne
      refine (fc x hx).prodMap' (fc y hy) <| isClosed_diagonal.isOpen_compl.mem_nhds ?_
      exact inj.ne hx hy hne

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
t : Set X
ht : t ∈ irreducibleComponents X
f : Y → X
hf₁ : Continuous[inst✝, inst✝¹] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
h : (t ∩ range f).Nonempty
u : Set Y
hu : IsIrreducible u
htu : f ⁻¹' t ⊆ u
⊢ t ⊆ closure[inst✝¹] (t ∩ range f)

Tactic:
exact subset_closure_inter_of_isPreirreducible_of_isOpen ht.1.2 hf₂.isOpen_range h

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst✝] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∉ U
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ

Tactic:
· rw [eventually_iff_exists_mem]
    use Uᶜ, hU.compl_mem_nhds h₁x
    intro y hy
    tauto_set

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
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
hf : Surjective f
inst✝ : PreirreducibleSpace X
⊢ IsPreirreducible (range f)

Tactic:
← Set.image_univ

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
hf : Surjective f
inst✝ : PreirreducibleSpace X
⊢ IsPreirreducible (f '' univ)
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
hf : Surjective f
inst✝ : IrreducibleSpace X
⊢ IsPreirreducible (range f)

Tactic:
← Set.image_univ

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
hf : Surjective f
inst✝ : IrreducibleSpace X
⊢ IsPreirreducible (f '' univ)
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:
rw [continuousWithinAt_Ioi_iff_Ici, continuousWithinAt_Iio_iff_Iic,
    continuousAt_iff_continuous_left_right]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
S : Set X
x : X
h : AccPt x (𝓟 S)
hs : S.Finite
this : Sᶜ ∈ codiscrete X
⊢ False

Tactic:
mem_codiscrete_accPt,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
S : Set X
x : X
h : AccPt x (𝓟 S)
hs : S.Finite
this : ∀ (x : X), ¬AccPt x (𝓟 Sᶜᶜ)
⊢ False
Module: Mathlib.Topology.Order.OrderClosed

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

Tactic:
by
  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.Order.OrderClosed

Goal state before:
pp: case neg
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
hx : ¬IsTop x
⊢ ∃ y ∈ s, x ≤ y

Tactic:
simp only [IsTop, not_forall, not_le] at hx
    rcases hs.exists_mem_open isOpen_Ioi hx with ⟨y, hys, hy : x < y⟩
    exact ⟨y, hys, hy.le⟩

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
s : ι → Set α
hs : IsPreconnected (⋃ n, s n)
hs' : ∀ (i : ι), IsOpen[inst✝] (s i)
i j : ι
hi : (s i).Nonempty
hj : (s j).Nonempty
⊢ TransGen (fun a b ↦ (s a ∩ s b).Nonempty) i j

Tactic:
by
  by_contra hij
  let S : Set ι := {k | TransGen (fun a b ↦ (s a ∩ s b).Nonempty) i k}
  let U : Set α := ⋃ k ∈ S, s k
  let V : Set α := ⋃ k ∈ Sᶜ, s k
  have hsplit : (⋃ n, s n) = U ∪ V := iSup_split s (· ∈ S)
  obtain ⟨a, ha⟩ := hi
  obtain ⟨b, hb⟩ := hj
  let hi_S : i ∈ S := Relation.TransGen.single ⟨a, ha, ha⟩
  have hUne : ((⋃ n, s n) ∩ U).Nonempty := ⟨a, mem_iUnion_of_mem i ha, mem_iUnion₂_of_mem hi_S ha⟩
  have hVne : ((⋃ n, s n) ∩ V).Nonempty := ⟨b, mem_iUnion_of_mem j hb, mem_iUnion₂_of_mem hij hb⟩
  obtain ⟨x, -, hxU, hxV⟩ := hs U V (isOpen_biUnion fun i a ↦ hs' i)
    (isOpen_biUnion fun i a ↦ hs' i) hsplit.le hUne hVne
  simp only [mem_iUnion, exists_prop, mem_compl_iff, U, V] at hxU hxV
  obtain ⟨k, hk, hxk⟩ := hxU
  obtain ⟨l, hl, hxl⟩ := hxV
  exact hl (hk.tail ⟨x, hxk, hxl⟩)

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

Goal state before:
pp: case mp
α : Type u_2
g : Set (Set α)
s : Set α
h : s ∈ countableGenerate g
⊢ ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s

pp: case mpr
α : Type u_2
g : Set (Set α)
s : Set α
h : ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s
⊢ s ∈ countableGenerate g

Tactic:
· induction h with
    | @basic s hs => exact ⟨{s}, by simp [hs]⟩
    | univ => exact ⟨∅, by simp⟩
    | superset _ _ ih => refine Exists.imp (fun S => ?_) ih; tauto
    | @sInter S Sct _ ih =>
      choose T Tg Tct hT using ih
      refine ⟨⋃ (s) (H : s ∈ S), T s H, by simpa, Sct.biUnion Tct, ?_⟩
      apply subset_sInter
      intro s H
      exact subset_trans (sInter_subset_sInter (subset_iUnion₂ s H)) (hT s H)

Goal state after:
case mpr
α : Type u_2
g : Set (Set α)
s : Set α
h : ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s
⊢ s ∈ countableGenerate g
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_3
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
      (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsuv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
rw [← not_nonempty_iff_eq_empty] at hsuv

Goal state after:
case refine_3
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
      (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsuv : ¬(s ∩ (u ∩ v)).Nonempty
⊢ s ⊆ u ∨ s ⊆ v
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst✝] (t i)) → ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
t : ι✝ → Set X
⊢ (∀ (i : ι✝), IsClosed[inst✝] (t i)) → univ ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ univ ∩ ⋂ i ∈ u, t i = ∅

Tactic:
simpa using h t

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

Goal state before:
pp: case right
X : Type u
Y : Type v
ι✝ : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t✝¹ : Set X
inst✝ : SecondCountableTopology X
t✝ : Set X
x✝¹ : t✝ ⊆ univ
x✝ : Filter X
ι : Type u
U : ι → Set X
hι : ∀ (i : ι), IsOpen[inst✝²] (U i)
hcover : t✝ ⊆ ⋃ i, U i
t : Set ι
htc : t.Countable
htu : ⋃ i ∈ t, U i = ⋃ i, U i
⊢ t✝ ⊆ ⋃ i ∈ t, U i

Tactic:
exact subset_of_subset_of_eq hcover (id htu.symm)

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed[inst✝¹] T'
hT₃ : T' ⊆ T
hT₄ : f ⁻¹' T' ∈ 𝓝 x
⊢ ∃ i, p i ∧ closure[inst✝¹] (f '' s i) ⊆ T

Tactic:
obtain ⟨i, hi, hi'⟩ := (h _).mp hT₄

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed[inst✝¹] T'
hT₃ : T' ⊆ T
hT₄ : f ⁻¹' T' ∈ 𝓝 x
i : ι
hi : p i
hi' : s i ⊆ f ⁻¹' T'
⊢ ∃ i, p i ∧ closure[inst✝¹] (f '' s i) ⊆ T
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
T : Set (Set X)
hT✝ : ∀ t ∈ T, IsOpen[inst✝] t
T_count : T.Countable
hT : T.Nonempty
f : ℕ → Set X
hf : T = range f
⊢ ∀ (n : ℕ), IsOpen[inst✝] (f n)

Tactic:
by simp_all

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
β : Type u_3
inst✝ : TopologicalSpace β
f : α → β
hf : IsCoinducing f
⊢ IsCoinducing ⋯.connectedComponentsMap

Tactic:
← ConnectedComponents.isQuotientMap_coe.isCoinducing.of_comp_iff

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
β : Type u_3
inst✝ : TopologicalSpace β
f : α → β
hf : IsCoinducing f
⊢ IsCoinducing (⋯.connectedComponentsMap ∘ ConnectedComponents.mk)