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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
⊢ AccPt x (𝓟 C) ↔ ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ C, y ≠ x

Tactic:
simp [accPt_principal_iff_clusterPt, clusterPt_principal_iff, Set.Nonempty,
    and_assoc]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case left
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
⊢ toIcoMod hp x₁ x₄ ≤ toIocMod hp x₁ x₃

Tactic:
suffices h : ¬x₃ ≡ x₂ [PMOD p] by
      have h₁₂₃' := toIxxMod_cyclic_left _ (toIxxMod_cyclic_left _ h₁₂₃.1)
      have h₂₃₄' := toIxxMod_cyclic_left _ (toIxxMod_cyclic_left _ h₂₃₄.1)
      rw [(not_modEq_iff_toIcoMod_eq_toIocMod hp).1 h] at h₂₃₄'
      exact toIxxMod_cyclic_left _ (h₁₂₃'.trans h₂₃₄')
    by_contra h
    rw [(modEq_iff_toIcoMod_eq_left hp).1 h] at h₁₂₃
    exact h₁₂₃.2 (left_lt_toIocMod _ _ _).le

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIocMod hp a (b + ↑m * p) = toIocMod hp a b

Tactic:
toIocMod_add_intCast_mul

Goal state after:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIocMod hp a b = toIocMod hp a b
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIcoMod hp a (b - ↑m * p) = toIcoMod hp a b

Tactic:
by
  simpa using toIcoMod_sub_zsmul hp a b m

Goal state after:
Module: Mathlib.Topology.Maps.OpenQuotient

Goal state before:
pp: case mp
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst✝¹] V
e : f ⁻¹' V = p ⁻¹' U
⊢ ∃ x, IsOpen[inst✝¹] (q ⁻¹' q '' x) ∧ g ⁻¹' q '' x = U

Tactic:
refine ⟨V, hq.continuous.1 _ (hq.isOpenMap _ hV), ?_⟩

Goal state after:
case mp
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst✝¹] V
e : f ⁻¹' V = p ⁻¹' U
⊢ g ⁻¹' q '' V = U
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
h : Subsingleton α
⊢ IndiscreteTopology α

Tactic:
infer_instance

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Y → Z
hf : IsOpenMap (f ∘ ⇑h)
⊢ IsOpenMap f

Tactic:
← Function.comp_id f,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Y → Z
hf : IsOpenMap (f ∘ ⇑h)
⊢ IsOpenMap (f ∘ id)
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)
x : X
s : Set X
hs : ClusterPt (f x) (𝓟 (f '' s)ᶜ)
⊢ comap f (𝓟 (f '' s)ᶜ) ≤ 𝓟 sᶜ

Tactic:
by simp [subset_preimage_image]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
⊢ 𝓝 (x, y) = 𝓝 x ×ˢ 𝓝 y

Tactic:
rw [prod_eq_inf, instTopologicalSpaceProd, nhds_inf (t₁ := TopologicalSpace.induced Prod.fst _)
    (t₂ := TopologicalSpace.induced Prod.snd _), nhds_induced, nhds_induced]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ιX : Type u_5
ιY : Type u_6
px : ιX → Prop
py : ιY → Prop
sx : ιX → Set X
sy : ιY → Set Y
x : X
y : Y
hx : (𝓝 x).HasBasis px sx
hy : (𝓝 y).HasBasis py sy
⊢ (𝓝 x ×ˢ 𝓝 y).HasBasis (fun i ↦ px i.1 ∧ py i.2) fun i ↦ sx i.1 ×ˢ sy i.2

Tactic:
exact hx.prod hy

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
h : t ⊆ s
⊢ 𝓝ˢ[t] s = 𝓟 t

Tactic:
simp [nhdsSetWithin, (principal_mono.2 h).trans principal_le_nhdsSet]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
f : X → Bool
b : Bool
⊢ Continuous[inst✝, _] f ↔ IsClopen (f ⁻¹' {b})

Tactic:
continuous_discrete_rng,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
f : X → Bool
b : Bool
⊢ (∀ (b : Bool), IsOpen[inst✝] (f ⁻¹' {b})) ↔ IsClopen (f ⁻¹' {b})
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
p✝ p q : X → Prop
hpq : p = q
x : X
⊢ p x → q (id x)

Tactic:
by simp [hpq]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
p✝ p q : X → Prop
hpq : p = q
x : X
⊢ q x → p (id x)

Tactic:
by simp [hpq]

Goal state after:
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
⊢ IsOpenMap (Sum.elim f g) ↔ IsOpenMap f ∧ IsOpenMap g

Tactic:
by
  simp only [isOpenMap_sum, elim_inl, elim_inr]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
t : Set ↑s
ht : IsClosed[instTopologicalSpaceSubtype] t
⊢ ∃ c, IsClosed[inst✝] c ∧ Subtype.val '' t = c ∩ s

Tactic:
simpa using IsInducing.subtypeVal.image_eq_isClosed_inter_range ht

Goal state after:
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)
C : Set Z
C_closed : IsClosed[inst✝] C
hC : Sum.elim f g ⁻¹' C = range inl
A : closure[inst✝] (range f) ⊆ C
⊢ Disjoint C (g '' univ)

Tactic:
disjoint_image_right,

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
A : closure[inst✝] (range f) ⊆ C
⊢ Disjoint (g ⁻¹' C) univ
Module: Mathlib.Topology.Bases

Goal state before:
pp: case inl
α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h✝ : IsEmpty α
⊢ SeparableSpace α

Tactic:
infer_instance

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:
infer_instance

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:
rw [nhds_prod_eq]; infer_instance

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

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

Goal state before:
pp: α : Type u_4
ι : Sort u_5
p : ι → Prop
l : Filter α
s : ι → Set α
q : Set α → Prop
hl : l.HasBasis p s
hq : ∀ ⦃s t : Set α⦄, s ⊆ t → q s → q t
⊢ (∃ᶠ (s : Set α) in l.smallSets, q s) ↔ ∀ (i : ι), p i → q (s i)

Tactic:
by
  rw [Filter.frequently_smallSets' hq, hl.forall_iff hq]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case a
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := ⋯
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ generateFrom (⋃ u ∈ s', f u) ≤ ts

Tactic:
hs'.eq_generateFrom

Goal state after:
case a
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ generateFrom (⋃ u ∈ s', f u) ≤ generateFrom s'
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: case inl
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y
s t : Set X✝
inst✝³ : SigmaCompactSpace X✝
inst✝² : Countable ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
h✝ : IsEmpty ι
⊢ SigmaCompactSpace ((i : ι) × X i)

Tactic:
infer_instance

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ ∃ n, K n ∈ 𝓝 x

Tactic:
rcases K.exists_mem x with ⟨n, hn⟩
  exact ⟨n + 1, mem_interior_iff_mem_nhds.mp <| K.subset_interior_succ n hn⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s : UpperSet α
⊢ ↑s = univ ↔ s = ⊥

Tactic:
by simp [SetLike.ext'_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s : UpperSet α
⊢ ↑s = ∅ ↔ s = ⊤

Tactic:
by simp [SetLike.ext'_iff]

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

Goal state before:
pp: case right
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
s : Finset ι
hs : u ⊆ ⋃ i ∈ s, Sigma.mk i '' Sigma.mk i ⁻¹' univ
x : (i : ι) × X i
⊢ (x ∈ (↑s).sigma fun i ↦ Sigma.mk i ⁻¹' u) ↔ x ∈ u

Tactic:
simp only [Set.mem_sigma_iff, Finset.mem_coe, Set.mem_preimage, and_iff_right_iff_imp]

Goal state after:
case right
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
s : Finset ι
hs : u ⊆ ⋃ i ∈ s, Sigma.mk i '' Sigma.mk i ⁻¹' univ
x : (i : ι) × X i
⊢ ⟨x.fst, x.snd⟩ ∈ u → x.fst ∈ s
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι), IsCompact (s i)
⊢ IsCompact (univ.pi s)

Tactic:
by
  convert! isCompact_pi_infinite h
  simp only [← mem_univ_pi, ofPred_mem_eq]

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_3
inst✝ : (d : ι) → TopologicalSpace (X d)
⊢ cocompact ((d : ι) → X d) ≤ Filter.coprodᵢ fun d ↦ cocompact (X d)

Tactic:
refine compl_surjective.forall.2 fun s H => ?_

Goal state after:
ι : Type u_1
X : ι → Type u_3
inst✝ : (d : ι) → TopologicalSpace (X d)
s : Set ((i : ι) → X i)
H : sᶜ ∈ Filter.coprodᵢ fun d ↦ cocompact (X d)
⊢ sᶜ ∈ cocompact ((d : ι) → X d)
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace Y
f : X → Y
K : Set Y
x✝ : IsCompact K
⊢ (∀ᶠ (x : X) in cofinite, f x ∈ Kᶜ) ↔ (f ⁻¹' K).Finite

Tactic:
simp only [mem_compl_iff, eventually_cofinite, not_not, preimage]

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

Tactic:
intro

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

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

Tactic:
intro

Goal state after:
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
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
a✝ : T2Space X
⊢ T0Space X

Tactic:
infer_instance

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

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

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Order.SuccPred.Relation

Goal state before:
pp: case refine_2.inl
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m✝ : α
hnm✝ : n ≤ m✝
m : α
hnm : n ≤ m
ih : (∀ i ∈ Ico n m, r i (succ i)) → ReflTransGen r n m
h : ∀ i ∈ Ico n (succ m), r i (succ i)
this : ReflTransGen r n m
hm : m = succ m
⊢ ReflTransGen r n (succ m)

Tactic:
rwa [← hm]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderClosedTopology α
f g : β → α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : (x : β) → Decidable (f x ≤ g x)
f' g' : β → γ
hf : Continuous[inst✝², inst✝⁵] f
hg : Continuous[inst✝², inst✝⁵] g
hf' : ContinuousOn f' {x | f x ≤ g x}
hg' : ContinuousOn g' {x | g x ≤ f x}
hfg : ∀ (x : β), f x = g x → f' x = g' x
⊢ Continuous[inst✝², inst✝¹] fun x ↦ if f x ≤ g x then f' x else g' x

Tactic:
by
  refine continuous_if (fun a ha => hfg _ (frontier_le_subset_eq hf hg ha)) ?_ (hg'.mono ?_)
  · rwa [(isClosed_le hf hg).closure_eq]
  · simp only [not_le]
    exact closure_lt_subset_le hg hf

Goal state after:
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
hc : IsCompact (f '' K \ interior s)
⊢ ∀ x_1 ∈ f '' K \ interior s, ¬Inseparable (f x) x_1

Tactic:
rintro y ⟨-, hys⟩ hxy

Goal state after:
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
hc : IsCompact (f '' K \ interior s)
y : Y
hys : y ∉ interior s
hxy : Inseparable (f x) y
⊢ False
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s t : Set α
Hs : IsConnected s
Ht : IsConnected t
x : α
hx : x ∈ s ∩ t
⊢ IsPreconnected (s ∪ t)

Tactic:
exact Hs.isPreconnected.union x (mem_of_mem_inter_left hx) (mem_of_mem_inter_right hx)
    Ht.isPreconnected

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

Goal state before:
pp: case refine_2
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
hc : IsCompact (f '' K \ interior s)
U V : Set Y
Uo : IsOpen[inst✝¹] U
Vo : IsOpen[inst✝¹] V
hxU : {f x} ⊆ U
hV : f '' K \ interior s ⊆ V
hd : Disjoint U V
y : X
hy : y ∈ K \ f ⁻¹' V
⊢ f y ∈ s

Tactic:
by_contra hys

Goal state after:
case refine_2
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
hc : IsCompact (f '' K \ interior s)
U V : Set Y
Uo : IsOpen[inst✝¹] U
Vo : IsOpen[inst✝¹] V
hxU : {f x} ⊆ U
hV : f '' K \ interior s ⊆ V
hd : Disjoint U V
y : X
hy : y ∈ K \ f ⁻¹' V
hys : f y ∉ s
⊢ False
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
hs : IsConnected s
i : ι
x : X i
hx : ⟨i, x⟩ ∈ s
this : s ⊆ range (mk i)
⊢ ∃ i t, IsConnected t ∧ s = mk i '' t

Tactic:
exact ⟨i, Sigma.mk i ⁻¹' s, hs.preimage_of_isOpenMap sigma_mk_injective isOpenMap_sigmaMk this,
      (Set.image_preimage_eq_of_subset this).symm⟩

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : s ⊆ f ⁻¹' (u ∪ v)
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
⊢ s ⊆ u' ∪ v'

Tactic:
preimage_union

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : s ⊆ f ⁻¹' u ∪ f ⁻¹' v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
⊢ s ⊆ u' ∪ v'
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x✝ : TopologicalSpace X := sInf T
a : X
⊢ (𝓝 a).HasBasis (fun If ↦ If.fst.Finite ∧ ∀ (i : ↑If.fst), If.snd i ∈ 𝓝 a ∧ IsClosed[↑↑i] (If.snd i)) fun If ↦
    ⋂ i, If.snd i

Tactic:
nhds_sInf,

Goal state after:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x✝ : TopologicalSpace X := sInf T
a : X
⊢ (⨅ t ∈ T, 𝓝 a).HasBasis (fun If ↦ If.fst.Finite ∧ ∀ (i : ↑If.fst), If.snd i ∈ 𝓝 a ∧ IsClosed[↑↑i] (If.snd i)) fun If ↦
    ⋂ i, If.snd i
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case inl
X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed[inst✝²] s
t_cl : IsClosed[inst✝²] t
st_dis : Disjoint s t
empty_X : IsEmpty X
⊢ _root_.HasSeparatingCover s t

Tactic:
rw [subset_eq_empty (t := s) (fun ⦃_⦄ _ ↦ trivial) (univ_eq_empty_iff.mpr empty_X)]
    exact hasSeparatingCovers_iff_separatedNhds.mpr (SeparatedNhds.empty_left t) |>.1

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

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

Tactic:
intro

Goal state after:
case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
a✝ : T3Space X
⊢ T0Space X
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
⊢ T0Space X → T3Space X

Tactic:
intro

Goal state after:
case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
a✝ : T0Space X
⊢ T3Space X
Module: Mathlib.Topology.Separation.Regular

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

Tactic:
infer_instance

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

Goal state before:
pp: case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
a✝ : T0Space X
⊢ T3Space X

Tactic:
infer_instance

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

Goal state before:
pp: case a.right
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
a : α
hat : a ∈ f ⁻¹' t
hav : a ∈ v
h : f ⁻¹' {f a} ⊆ u
⊢ False

Tactic:
exact uv_disj.subset_compl_left hav (h rfl)

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
ι : Type u_3
ι' : Sort u_4
inst✝ : TopologicalSpace X
⊢ CountableInterFilter (countableGenerate {t | IsOpen[inst✝] t ∧ Dense t})

Tactic:
infer_instance

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

Goal state before:
pp: X : Type u_1
Y✝ : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y✝
inst✝⁵ : TopologicalSpace W
inst✝⁴ : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝³ : TopologicalSpace X'
inst✝² : TopologicalSpace Y'
ι : Type u_7
inst✝¹ : DecidableEq ι
i : ι
Y : ι → Type u_8
inst✝ : (j : ι) → TopologicalSpace (Y j)
j : ι
⊢ Continuous[instTopologicalSpaceProd, inst✝ j] fun a ↦ (Equiv.piSplitAt i Y).invFun a j

Tactic:
by
      dsimp only [Equiv.piSplitAt]
      split_ifs with h
      · subst h
        exact continuous_fst
      · exact (continuous_apply _).comp continuous_snd

Goal state after: