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

Goal state before:
pp: case refl.refine_1
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
h : IsOpen[⊤] U
⊢ U = ∅ ∨ U = univ

pp: case refl.refine_2
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
⊢ U = ∅ ∨ U = univ → IsOpen[⊤] U

Tactic:
· induction h with
    | basic _ h => exact False.elim h
    | univ => exact .inr rfl
    | inter _ _ _ _ h₁ h₂ =>
      rcases h₁ with (rfl | rfl) <;> rcases h₂ with (rfl | rfl) <;> simp
    | sUnion _ _ ih => exact sUnion_mem_empty_univ ih

Goal state after:
case refl.refine_2
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
⊢ U = ∅ ∨ U = univ → IsOpen[⊤] U
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:
by
  simp only [← isOpen_compl_iff, isOpen_coinduced (f := f), preimage_compl]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : IndiscreteTopology α
x : α
f : Filter α
inst✝ : f.NeBot
⊢ ClusterPt x f

Tactic:
by
  simpa [ClusterPt, IndiscreteTopology.nhds_eq]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ IsClosed[inst✝] (⇑h '' s) ↔ IsClosed[inst✝¹] s

Tactic:
by
  rw [← preimage_symm, isClosed_preimage]

Goal state after:
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
hf : IsInducing f
h : IsClosed[inst✝] (range f)
⊢ IsClosedMap f

Tactic:
intro s hs
  rcases hf.isClosed_iff.1 hs with ⟨t, ht, rfl⟩
  rw [image_preimage_eq_inter_range]
  exact ht.inter h

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_5
I : Set ι
hI : I.Finite
s : ι → Set α
a : α
⊢ 𝓝[⋃ i ∈ I, s i] a = ⨆ i ∈ I, 𝓝[s i] a

Tactic:
induction I, hI using Set.Finite.induction_on with

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝[{a}ᶜ ∪ {a}] a = 𝓝 a

Tactic:
compl_union_self,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝[univ] a = 𝓝 a
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case inr.mp.refine_1
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : IsOpen[instTopologicalSpaceProd] (s ×ˢ t)
⊢ IsOpen[inst✝¹] s

Tactic:
simpa only [fst_image_prod _ st.2] using isOpenMap_fst _ H

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ ClusterPt a (𝓟 J) ↔ ∃ᶠ (x : α) in 𝓝[t] ↑a, ∃ (h : x ∈ s), ⟨x, h⟩ ∈ J

Tactic:
by
  rw [nhdsWithin_eq_map_subtype_coe (hst a.prop), Filter.frequently_map,
    clusterPt_principal_iff_frequently,
    Topology.IsInducing.subtypeVal.nhds_eq_comap, Filter.frequently_comap,
    Topology.IsInducing.subtypeVal.nhds_eq_comap, Filter.frequently_comap, Subtype.coe_mk]
  apply frequently_congr
  apply Eventually.of_forall
  intro x
  simp only [SetCoe.exists, exists_and_left, exists_eq_left]
  exact ⟨fun ⟨h, hx⟩ => ⟨hst h, h, hx⟩, fun ⟨_, hx⟩ => hx⟩

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
hf : ContinuousOn f s
hs : IsOpen[inst✝¹] s
⊢ interior (s ∩ f ⁻¹' t) = s ∩ interior (f ⁻¹' t)

Tactic:
by rw [interior_inter, hs.interior_eq]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s : Set α
⊢ 𝓝ˢ s = comap f (𝓝ˢ (f '' s))

Tactic:
ext s
  rw [mem_nhdsSet_induced, mem_comap]

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

Goal state after:
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 ↔ ∀ (a : α), IsOpenMap fun x ↦ f (a, x)

Tactic:
simp_rw [isOpenMap_iff_nhds_le, Prod.forall, nhds_prod_eq, nhds_discrete, pure_prod, map_map]
  rfl

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : Y → (j : Fin n) → A j.castSucc
g : Y → A (Fin.last n)
l : Filter Y
x : (j : Fin n) → A j.castSucc
y : A (Fin.last n)
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ ∀ (i : Fin n), Tendsto (fun i_1 ↦ Fin.snoc (f i_1) (g i_1) i.castSucc) l (𝓝 (Fin.snoc x y i.castSucc))

Tactic:
by simpa using tendsto_pi_nhds.1 hf

Goal state after:
Module: Mathlib.Order.SetAccumulate

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

Tactic:
simp at hk

Goal state after:
case succ
α : 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
⊢ ∃ m, accumulate s (n + 1) ⊆ s m
Module: Mathlib.Topology.Bornology.Basic

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
singleton_mem : ∀ (x : α), {x} ∈ B
⊢ comk (fun x ↦ x ∈ B) empty_mem subset_mem union_mem ≤ cofinite

Tactic:
by simpa [le_cofinite_iff_compl_singleton_mem]

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

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (a : α), ∃ b ∈ B, a ∈ b
x : α
⊢ {x} ∈ B

Tactic:
rcases sUnion_univ x with ⟨s, hs, hxs⟩

Goal state after:
ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (a : α), ∃ b ∈ B, a ∈ b
x : α
s : Set α
hs : s ∈ B
hxs : x ∈ s
⊢ {x} ∈ B
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_1
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
⊢ Pi.topologicalSpace ≤ generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s}

pp: case refine_2
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
⊢ generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s} ≤ Pi.topologicalSpace

Tactic:
· apply le_generateFrom
    rintro _ ⟨s, i, hi, rfl⟩
    let := fun a => generateFrom (g a)
    exact isOpen_set_pi i.finite_toSet (fun a ha => GenerateOpen.basic _ (hi a ha))

Goal state after:
case refine_2
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
⊢ generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s} ≤ Pi.topologicalSpace
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
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
κ : Type u_8
inst✝⁴ : TopologicalSpace X
T : (i : ι) → TopologicalSpace (A i)
inst✝³ : (i : ι) → TopologicalSpace (B i)
f : X → (i : ι) → A i
inst✝² : TopologicalSpace Z
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), DiscreteTopology (A i)
x : (i : ι) → A i
⊢ IsOpen[topologicalSpace] {x}

Tactic:
rw [← univ_pi_singleton]

Goal state after:
X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
κ : Type u_8
inst✝⁴ : TopologicalSpace X
T : (i : ι) → TopologicalSpace (A i)
inst✝³ : (i : ι) → TopologicalSpace (B i)
f : X → (i : ι) → A i
inst✝² : TopologicalSpace Z
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), DiscreteTopology (A i)
x : (i : ι) → A i
⊢ IsOpen[topologicalSpace] (univ.pi fun i ↦ {x i})
Module: Mathlib.Topology.Bases

Goal state before:
pp: case inl
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen[inst✝ i] U}
h : (↑s).pi U = ∅
⊢ IsOpen[inst✝ i] (eval i '' (↑s).pi U)

Tactic:
simp [h]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
p : Set X → Prop
he : p ∅
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
⊢ p s

Tactic:
let f : Filter X := comk p he (fun _t ht _s hsub ↦ hmono hsub ht) (fun _s hs _t ht ↦ hunion hs ht)

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
p : Set X → Prop
he : p ∅
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := comk p he ⋯ ⋯
⊢ p 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

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

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s s' : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : n ∈ 𝓝ˢ[s'] s ×ˢ 𝓟 t
⊢ ∃ u ∈ 𝓝ˢ[s'] s, u ×ˢ t ⊆ n

Tactic:
Filter.mem_prod_principal

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s s' : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : {a | ∀ b ∈ t, (a, b) ∈ n} ∈ 𝓝ˢ[s'] s
⊢ ∃ u ∈ 𝓝ˢ[s'] s, u ×ˢ t ⊆ n
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s,
      ∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s, y ∈ closure[inst✝] {x}, closure[inst✝] {y} ⊆ closure[inst✝] {x},
      ClusterPt y (pure x)].TFAE

Tactic:
tfae_have 1 → 2 := (pure_le_nhds _).trans
  tfae_have 2 → 3 := fun h s hso hy => h (hso.mem_nhds hy)
  tfae_have 3 → 4 := fun h s hsc hx => of_not_not fun hy => h sᶜ hsc.isOpen_compl hy hx
  tfae_have 4 → 5 := fun h => h _ isClosed_closure (subset_closure <| mem_singleton _)
  tfae_have 6 ↔ 5 := isClosed_closure.closure_subset_iff.trans singleton_subset_iff
  tfae_have 5 ↔ 7 := by
    rw [mem_closure_iff_clusterPt, principal_singleton]
  tfae_have 5 → 1 := by
    refine fun h => (nhds_basis_opens _).ge_iff.2 ?_
    rintro s ⟨hy, ho⟩
    rcases mem_closure_iff.1 h s ho hy with ⟨z, hxs, rfl : z = x⟩
    exact ho.mem_nhds hxs
  tfae_finish

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
H : ∀ (x : Y), IsDiscrete (f ⁻¹' {x})
x : X
hx : x ∈ f ⁻¹' s
h : 𝓝 x ⊓ 𝓟 (f ⁻¹' {f x}) ≤ pure x
⊢ 𝓝[f ⁻¹' s] x ≤ pure x

Tactic:
← comap_pure,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
H : ∀ (x : Y), IsDiscrete (f ⁻¹' {x})
x : X
hx : x ∈ f ⁻¹' s
h : 𝓝 x ⊓ comap f (pure (f x)) ≤ pure x
⊢ 𝓝[f ⁻¹' s] x ≤ pure x
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
⊢ False

Tactic:
have := hs.compl_mem_codiscrete

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 : Sᶜ ∈ codiscrete X
⊢ False
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: ι : Type u_3
β : ι → Type u_4
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → TopologicalSpace (β i)
x : (i : ι) → β i
i : ι
inst✝ : ∀ (i : ι), T1Space (β i)
s : Set (β i)
hs : IsClosed[inst✝¹ i] s
⊢ ∀ a ∈ univ, IsClosed[inst✝¹ a] (update (fun j ↦ {x j}) i s a)

Tactic:
simp [forall_update_iff, hs]

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

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

Tactic:
simp [h]

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

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

Tactic:
simp [h]

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

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

Tactic:
simp [h]

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

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

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝³ : TopologicalSpace α
s t u v : Set α
inst✝² : TopologicalSpace β
inst✝¹ : LocallyConnectedSpace α
inst✝ : LocallyConnectedSpace β
⊢ LocallyConnectedSpace (α × β)

Tactic:
rw [locallyConnectedSpace_iff_connected_subsets]
  rintro ⟨x, y⟩ U hU
  obtain ⟨u, hu, v, hv, huv⟩ := mem_nhds_prod_iff.mp hU
  exact ⟨connectedComponentIn u x ×ˢ connectedComponentIn v y,
    prod_mem_nhds (connectedComponentIn_mem_nhds hu) (connectedComponentIn_mem_nhds hv),
    isPreconnected_connectedComponentIn.prod isPreconnected_connectedComponentIn,
    (prod_mono (connectedComponentIn_subset _ _) (connectedComponentIn_subset _ _)).trans huv⟩

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

Goal state before:
pp: case pos
ι : Type u_1
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyConnectedSpace (X i)
hfinite : {i | ¬PreconnectedSpace (X i)}.Finite
x : (i : ι) → X i
U : Set ((i : ι) → X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PreconnectedSpace (X i)}
i : ι
hi : i ∈ K
⊢ IsPreconnected (K.piecewise (fun i ↦ connectedComponentIn (t i) (x i)) (fun x ↦ univ) i)

Tactic:
piecewise_eq_of_mem _ _ _ hi

Goal state after:
case pos
ι : Type u_1
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyConnectedSpace (X i)
hfinite : {i | ¬PreconnectedSpace (X i)}.Finite
x : (i : ι) → X i
U : Set ((i : ι) → X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PreconnectedSpace (X i)}
i : ι
hi : i ∈ K
⊢ IsPreconnected (connectedComponentIn (t i) (x i))
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case h₁
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : S.Countable
s t : (s : Set α) → s ∈ S → Set α
hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
hs : ⋂ i, ⋂ (h : i ∈ S), s i h ∈ l₁
ht : ⋂ i, ⋂ (h : i ∈ S), t i h ∈ l₂
i : Set α
hi : i ∈ S
⊢ ⋂ i, ⋂ (h : i ∈ S), s i h ⊆ s i hi

Tactic:
exact iInter_subset_of_subset i (iInter_subset _ _)

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

Goal state before:
pp: case h₂
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : S.Countable
s t : (s : Set α) → s ∈ S → Set α
hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
hs : ⋂ i, ⋂ (h : i ∈ S), s i h ∈ l₁
ht : ⋂ i, ⋂ (h : i ∈ S), t i h ∈ l₂
i : Set α
hi : i ∈ S
⊢ ⋂ i, ⋂ (h : i ∈ S), t i h ⊆ t i hi

Tactic:
exact iInter_subset_of_subset i (iInter_subset _ _)

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

Goal state before:
pp: case left
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U ↑x
⊢ ∀ x ∈ Subtype.val '' t, x ∈ s

pp: case right
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U ↑x
⊢ s ⊆ ⋃ x ∈ Subtype.val '' t, U x

Tactic:
· intro _
    simp only [mem_image, Subtype.exists, exists_and_right, exists_eq_right, forall_exists_index]
    tauto

Goal state after:
case right
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U ↑x
⊢ s ⊆ ⋃ x ∈ Subtype.val '' t, U x
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
K : Set X
hK : IsCompact K
⊢ (𝓝ˢ K).lift' closure[inst✝¹] = 𝓝ˢ K

Tactic:
refine le_antisymm (fun U hU ↦ ?_) (le_lift'_closure _)

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : U ∈ 𝓝ˢ K
⊢ U ∈ (𝓝ˢ K).lift' closure[inst✝¹]
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case insert
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ univ.pi s
hgv : g ∈ v
i : ι
I : Finset ι
a✝ : i ∉ I
ihI : I.piecewise f g ∈ u → (univ.pi s ∩ (u ∩ v)).Nonempty
hI : update (I.piecewise f g) i (f i) ∈ u
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty

Tactic:
have := I.piecewise_mem_set_pi hfs hgs

Goal state after:
case insert
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ univ.pi s
hgv : g ∈ v
i : ι
I : Finset ι
a✝ : i ∉ I
ihI : I.piecewise f g ∈ u → (univ.pi s ∩ (u ∩ v)).Nonempty
hI : update (I.piecewise f g) i (f i) ∈ u
this : I.piecewise f g ∈ univ.pi s
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsInducing e
s t : Set X
hd₁ : Disjoint (closure[inst✝²] s) t
hd₂ : Disjoint s (closure[inst✝²] t)
⊢ Disjoint (closure[inst✝¹] (e '' s)) (e '' t)

Tactic:
← subset_compl_iff_disjoint_left,

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsInducing e
s t : Set X
hd₁ : Disjoint (closure[inst✝²] s) t
hd₂ : Disjoint s (closure[inst✝²] t)
⊢ e '' t ⊆ (closure[inst✝¹] (e '' s))ᶜ
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case right
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
ι : Type u_2
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst✝¹] (U i)
this : IsLindelof (⋃ i, U i)
t : Set ι
htc : t.Countable
htu : ⋃ i, U i ⊆ ⋃ i ∈ t, U i
⊢ ⋃ i ∈ t, U i = ⋃ i, U i

Tactic:
apply eq_of_subset_of_subset (iUnion₂_subset_iUnion (fun i ↦ i ∈ t) fun i ↦ U i) htu

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsOpen[inst✝] s
⊢ ∀ t ∈ {s}, IsOpen[inst✝] t

Tactic:
simp [h]

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

Goal state before:
pp: case inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set (Set X)
ho : ∀ s ∈ S, IsOpen[inst✝¹] s
hS : S.Countable
hd : ∀ s ∈ S, Dense s
h : S = ∅
⊢ Dense (⋂₀ S)

Tactic:
simp [h]

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

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
⊢ instTopologicalSpaceUnits = TopologicalSpace.induced val inst✝

Tactic:
topology_eq_inf,

Goal state after:
M : Type u_4
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
⊢ TopologicalSpace.induced val inst✝ ⊓ TopologicalSpace.induced (fun u ↦ ↑u⁻¹) inst✝ =
    TopologicalSpace.induced val inst✝
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: case succ
α : Type ua
inst✝ : UniformSpace α
n✝ : ℕ
ihn : ∀ {s : SetRel α α}, s ∈ 𝓤 α → ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x ↦ t ○ x)^[n✝] t ⊆ s
s : SetRel α α
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
U : SetRel α α
hU : U ⊆ t ∧ (fun x ↦ U ○ x)^[n✝] U ⊆ t
⊢ U ⊆ s ∧ (fun x ↦ U ○ x)^[n✝ + 1] U ⊆ s

Tactic:
rw [Function.iterate_succ_apply']

Goal state after:
case succ
α : Type ua
inst✝ : UniformSpace α
n✝ : ℕ
ihn : ∀ {s : SetRel α α}, s ∈ 𝓤 α → ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x ↦ t ○ x)^[n✝] t ⊆ s
s : SetRel α α
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
U : SetRel α α
hU : U ⊆ t ∧ (fun x ↦ U ○ x)^[n✝] U ⊆ t
⊢ U ⊆ s ∧ U ○ (fun x ↦ U ○ x)^[n✝] U ⊆ s
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: β : Type ub
U : SetRel β β
inst✝ : U.IsSymm
s N : Set β
⊢ U.IsCover s N ↔ s ⊆ ⋃ y ∈ N, ball y U

Tactic:
by
  simp [SetRel.IsCover, subset_def, ball, U.comm]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ i, s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
x : α
hx : x ∈ t
i : ι
hi : x ∈ s i
⊢ ∃ i, t ⊆ s i

Tactic:
refine ⟨i, fun y hy => ?_⟩

Goal state after:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ i, s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
x : α
hx : x ∈ t
i : ι
hi : x ∈ s i
y : α
hy : y ∈ t
⊢ y ∈ s i
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
x : α
⊢ 𝓝 x = comap (Prod.mk x) ⊤

Tactic:
simp only [nhds_top, comap_top]

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s t : Set α
hf : UniformContinuousOn f s
ht : t ⊆ s
⊢ 𝓟 (t ×ˢ t) ≤ 𝓟 (s ×ˢ s)

Tactic:
simp [ht]

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : IsUniformInducing f
hsurj : Surjective f
⊢ CompleteSpace α ↔ CompleteSpace β

Tactic:
rw [completeSpace_iff_isComplete_range hf, hsurj.range_eq, completeSpace_iff_isComplete_univ]

Goal state after: