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

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
p : α → Prop
⊢ (∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y) ↔ ∀ᶠ (x : α) in atTop, p x

Tactic:
refine ⟨fun h ↦ h.mono fun x hx ↦ hx x le_rfl, fun h ↦ ?_⟩
  rcases (hasBasis_iInf_principal_finite _).eventually_iff.1 h with ⟨S, hSf, hS⟩
  refine mem_iInf_of_iInter hSf (V := fun x ↦ Ici x.1) (fun _ ↦ Subset.rfl) fun x hx y hy ↦ ?_
  simp only [mem_iInter] at hS hx
  exact hS fun z hz ↦ le_trans (hx ⟨z, hz⟩) hy

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hn : n ≠ 0
hp : ∀ k < n, ∀ᶠ (a : ℕ) in atTop, p (n * a + k)
⊢ ∀ᶠ (a : ℕ) in atTop, p a

Tactic:
simp only [eventually_atTop] at hp ⊢
  choose! N hN using hp
  refine ⟨(Finset.range n).sup (n * N ·), fun b hb => ?_⟩
  rw [← Nat.div_add_mod b n]
  have hlt := Nat.mod_lt b hn.bot_lt
  refine hN _ hlt _ ?_
  rw [Nat.le_div_iff_mul_le hn.bot_lt, mul_comm]
  exact (Finset.le_sup (f := (n * N ·)) (Finset.mem_range.2 hlt)).trans hb

Goal state after:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ∈ n.factorization.support
h : 0 < n.factorization p
⊢ φ (p ^ n.factorization p) = p ^ (n.factorization p - 1) * (p - 1)

Tactic:
totient_prime_pow (prime_of_mem_primeFactors hp) h

Goal state after:
n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ∈ n.factorization.support
h : 0 < n.factorization p
⊢ p ^ (n.factorization p - 1) * (p - 1) = p ^ (n.factorization p - 1) * (p - 1)
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: case refine_2
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirectedOrder α
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun n ↦ List.foldl (fun x n ↦ c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
⊢ Tendsto xs atTop atTop

Tactic:
· refine (tendsto_add_atTop_iff_nat 1).1 <| tendsto_atTop_mono (fun n ↦ ?_) h
    rw [hsucc]
    apply hright

Goal state after:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a : ℕ
ha : ¬a = 0
c : ℕ
h' : φ a = φ (a * c)
hb : ¬a * c = 0
this : a.Coprime c
⊢ a = a * c ∨ 2 * a = a * c

Tactic:
by
    rw [totient_mul this, eq_comm, mul_eq_left (totient_eq_zero.not.mpr ha),
      totient_eq_one_iff] at h'
    obtain rfl | rfl := h'
    · simp
    · simp [mul_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
h : Set α → Set β
m : γ → β
l : Filter γ
⊢ Tendsto m l (f.lift' h) ↔ ∀ s ∈ f, ∀ᶠ (a : γ) in l, m a ∈ h s

Tactic:
simp only [Filter.lift', tendsto_lift, tendsto_principal, comp]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
ι : Type u_1
s : Set ι
hs : s.Finite
f : ι → Set X
⊢ closure (⋃ i ∈ s, f i) = ⋃ i ∈ s, closure (f i)

Tactic:
simp [closure_eq_compl_interior_compl, hs.interior_biInter]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: case mpr
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
x : X
⊢ x ∈ closure s

Tactic:
rw [mem_closure_iff]

Goal state after:
case mpr
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
x : X
⊢ ∀ (o : Set X), IsOpen o → x ∈ o → (o ∩ s).Nonempty
Module: Mathlib.Topology.Closure

Goal state before:
pp: case mpr
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
x : X
U : Set X
⊢ IsOpen U → x ∈ U → (U ∩ s).Nonempty

Tactic:
U_op

Goal state after:
case mpr
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
x : X
U : Set X
U_op : IsOpen U
⊢ x ∈ U → (U ∩ s).Nonempty
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
⊢ interior (frontier s) = ∅

Tactic:
have B : interior (frontier s) ⊆ interior s := by rw [A]; exact interior_mono sdiff_subset

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
⊢ interior (frontier s) = ∅
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 c : α
h₁₂₃ : toIcoMod hp a b ≤ toIocMod hp a c
h₁₃₂ : toIcoMod hp a c ≤ toIocMod hp a b
⊢ b ≡ a [PMOD p] ∨ c ≡ b [PMOD p] ∨ a ≡ c [PMOD p]

Tactic:
by_contra! h
  rw [modEq_comm] at h
  rw [← (not_modEq_iff_toIcoMod_eq_toIocMod hp).mp h.2.2] at h₁₂₃
  rw [← (not_modEq_iff_toIcoMod_eq_toIocMod hp).mp h.1] at h₁₃₂
  exact h.2.1 ((toIcoMod_inj _).1 <| h₁₃₂.antisymm h₁₂₃)

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
f : Filter X
⊢ IsClosed[inst✝] {x | ClusterPt x f}

Tactic:
simp only [clusterPt_iff_forall_mem_closure, ofPred_forall]
  exact isClosed_biInter fun _ _ ↦ isClosed_closure

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

Goal state before:
pp: case H.H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
z✝² z✝¹ z✝ : α
h₁₂₃ : toIcoMod ⋯ z✝² z✝¹ ≤ toIocMod ⋯ z✝² z✝
h₃₂₁ : toIcoMod ⋯ z✝² z✝ ≤ toIocMod ⋯ z✝² z✝¹
⊢ ↑z✝² = ↑z✝¹ ∨ ↑z✝¹ = ↑z✝ ∨ ↑z✝ = ↑z✝²

Tactic:
← modEq_iff_eq_mod_zmultiples

Goal state after:
case H.H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
z✝² z✝¹ z✝ : α
h₁₂₃ : toIcoMod ⋯ z✝² z✝¹ ≤ toIocMod ⋯ z✝² z✝
h₃₂₁ : toIcoMod ⋯ z✝² z✝ ≤ toIocMod ⋯ z✝² z✝¹
⊢ z✝² ≡ z✝¹ [PMOD p] ∨ z✝¹ ≡ z✝ [PMOD p] ∨ z✝ ≡ z✝² [PMOD p]
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ Disjoint (𝓟 t) (𝓝ˢ s) ↔ Disjoint s (closure[inst✝] t)

Tactic:
disjoint_principal_nhdsSet,

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ Disjoint (closure[inst✝] t) s ↔ Disjoint s (closure[inst✝] t)
Module: Mathlib.Topology.Bases

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

Tactic:
rw [hB.open_eq_sUnion' hs]

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

Goal state before:
pp: case refine_2
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : ∀ (U : Set X), IsOpen[inst✝] U → U.Nonempty → (U ∩ s).Nonempty
v : Set X
hv1 : IsOpen[inst✝] v
t : Set X
ht : IsOpen[inst✝] t
ht' : t.Nonempty
hud : ∀ (U : Set ↑s), IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ Subtype.val ⁻¹' v).Nonempty
⊢ (s ↓∩ t).Nonempty

Tactic:
· obtain ⟨x, hx⟩ := hs t ht ht'
    simpa using ⟨⟨x, hx.2⟩, hx.1⟩

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_5
s : ι → Set α
hf : ∀ (i : ι), ContinuousOn f (s i)
hs : ∀ (i : ι), IsOpen[inst✝¹] (s i)
hs' : ⋃ i, s i = univ
⊢ ContinuousOn f univ

Tactic:
← hs'

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_5
s : ι → Set α
hf : ∀ (i : ι), ContinuousOn f (s i)
hs : ∀ (i : ι), IsOpen[inst✝¹] (s i)
hs' : ⋃ i, s i = univ
⊢ ContinuousOn f (⋃ i, s i)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
⊢ ∃ b, IsTopologicalBasis (range b)

Tactic:
obtain ⟨t, ht⟩ := TopologicalSpace.exists_countable_basis α

Goal state after:
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : t.Countable ∧ ∅ ∉ t ∧ IsTopologicalBasis t
⊢ ∃ b, IsTopologicalBasis (range b)
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι
s : ι → Set X
hcomp✝ : ∀ (i : ι), IsSigmaCompact (s i)
K : ι → ℕ → Set X
hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)
hcov : ∀ (i : ι), ⋃ n, K i n = s i
this : ⋃ i, s i = ⋃ x, Function.uncurry K x
⊢ IsSigmaCompact (⋃ i, s i)

Tactic:
rw [this]

Goal state after:
X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι
s : ι → Set X
hcomp✝ : ∀ (i : ι), IsSigmaCompact (s i)
K : ι → ℕ → Set X
hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)
hcov : ∀ (i : ι), ⋃ n, K i n = s i
this : ⋃ i, s i = ⋃ x, Function.uncurry K x
⊢ IsSigmaCompact (⋃ x, Function.uncurry K x)
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: 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)
⊢ SigmaCompactSpace ((i : ι) × X i)

Tactic:
cases isEmpty_or_nonempty ι
  · infer_instance
  · rcases exists_surjective_nat ι with ⟨f, hf⟩
    refine ⟨⟨fun n => ⋃ k ≤ n, Sigma.mk (f k) '' compactCovering (X (f k)) n, fun n => ?_, ?_⟩⟩
    · refine (finite_le_nat _).isCompact_biUnion fun k _ => ?_
      exact (isCompact_compactCovering _ _).image continuous_sigmaMk
    · simp only [iUnion_eq_univ_iff, Sigma.forall, mem_iUnion, hf.forall]
      intro k y
      rcases exists_mem_compactCovering y with ⟨n, hn⟩
      refine ⟨max k n, k, le_max_left _ _, mem_image_of_mem _ ?_⟩
      exact compactCovering_subset _ (le_max_right _ _) hn

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Finset ↑s
ht : ⋃ x ∈ t, U ↑x ∈ 𝓝ˢ s
⊢ ∃ t, (∀ x ∈ t, x ∈ s) ∧ ⋃ x ∈ t, U x ∈ 𝓝ˢ s

Tactic:
exact ⟨t.image (↑), fun x hx =>
    let ⟨y, _, hyx⟩ := Finset.mem_image.1 hx
    hyx ▸ y.2,
    by rwa [Finset.set_biUnion_finset_image]⟩

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

Goal state before:
pp: α : Type u_2
A : Set α
T : Set (Set ↑A)
⊢ Subtype.val '' ⋃₀ T = ⋃₀ {x | ∃ B ∈ T, Subtype.val '' B = x}

Tactic:
rw [image_sUnion, image]

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : SpecializingMap f
hg : SpecializingMap g
⊢ SpecializingMap (g ∘ f)

Tactic:
by
  simp only [specializingMap_iff_stableUnderSpecialization_image, Set.image_comp] at *
  exact fun s h ↦ hg _ (hf _ h)

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
⊢ IsOpen[inst✝¹] {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}

Tactic:
refine isOpen_iff_mem_nhds.mpr fun a ha => ?_

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
a : X
ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
⊢ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y} ∈ 𝓝 a
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: 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
this : ∀ᶠ (x : X × X) in 𝓝ˢ (s ×ˢ s), f x.1 = f x.2 → x.1 = x.2
⊢ ∃ t ∈ 𝓝ˢ s, InjOn f t

Tactic:
sc.nhdsSet_prod_eq sc

Goal state after:
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
this : ∀ᶠ (x : X × X) in 𝓝ˢ s ×ˢ 𝓝ˢ s, f x.1 = f x.2 → x.1 = x.2
⊢ ∃ t ∈ 𝓝ˢ s, InjOn f t
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
⊢ 𝓝ˢ s ≤ 𝓝ˢ t ∧ 𝓝ˢ t ≤ 𝓝ˢ s ↔ s ⊆ t ∧ t ⊆ s

Tactic:
exact and_congr nhdsSet_le_iff nhdsSet_le_iff

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

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

Tactic:
by
  simp [codiscrete, mem_codiscreteWithin, compl_eq_univ_sdiff]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst✝¹] U
hKU : K ⊆ U
⊢ closure[inst✝¹] K ⊆ U

Tactic:
rw [hK.closure_eq_biUnion_inseparable, iUnion₂_subset_iff]
  exact fun x hx y hxy ↦ (hxy.mem_open_iff hU).1 (hKU hx)

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

Goal state before:
pp: case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : S ⊆ {s | sᶜ ∈ l}
⊢ ⋂₀ S ∈ {s | sᶜ ∈ l}

pp: case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : s ∈ {s | sᶜ ∈ l}
hsub : s ⊆ t
⊢ t ∈ {s | sᶜ ∈ l}

Tactic:
· rw [mem_ofPred_eq, compl_sInter]
    apply hUnion (compl '' S) (hSc.image _)
    intro s hs
    rw [mem_image] at hs
    rcases hs with ⟨t, ht, rfl⟩
    apply hSp ht

Goal state after:
case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : s ∈ {s | sᶜ ∈ l}
hsub : s ⊆ t
⊢ t ∈ {s | sᶜ ∈ l}
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: case refine_1.inr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h : LocallyConnectedSpace ((i : ι) → X i)
x : (i : ι) → X i
⊢ IsEmpty ((i : ι) → X i) ∨ (∀ (i : ι), LocallyConnectedSpace (X i)) ∧ {i | ¬PreconnectedSpace (X i)}.Finite

Tactic:
have : ∀ i, Nonempty (X i) := Classical.nonempty_pi.mp ⟨x⟩
    refine .inr ⟨fun i ↦ ((isOpenMap_eval i).isQuotientMap (continuous_apply i)
      (Function.surjective_eval i)).locallyConnectedSpace, ?_⟩
    have hVn : connectedComponent x ∈ 𝓝 x :=
      isOpen_connectedComponent.mem_nhds mem_connectedComponent
    rw [nhds_pi, Filter.mem_pi] at hVn
    obtain ⟨J, hJ, t, ht, htV⟩ := hVn
    refine hJ.subset fun i hi ↦ by_contra fun hiJ ↦ hi ?_
    suffices himg : Function.eval i '' connectedComponent x = univ from
      ⟨himg ▸ isPreconnected_connectedComponent.image _ (continuous_apply i).continuousOn⟩
    refine (subset_univ _).antisymm fun z _ ↦ ⟨Function.update x i z, htV fun j hj ↦ ?_, by simp⟩
    rw [Function.update_of_ne (ne_of_mem_of_not_mem hj hiJ)]
    exact mem_of_mem_nhds (ht j)

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

Goal state before:
pp: ι : 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
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty

Tactic:
rcases exists_finset_piecewise_mem_of_mem_nhds (uo.mem_nhds hfu) g with ⟨I, hI⟩

Goal state after:
ι : 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 : Finset ι
hI : I.piecewise f g ∈ u
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty
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
this : I.piecewise f g ∈ univ.pi s
h : I.piecewise f g ∈ v
S : Set ((a : ι) → X a) := update (I.piecewise f g) i '' s i
hsub : S ⊆ univ.pi s
hconn : IsPreconnected S
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty

Tactic:
have hSu : (S ∩ u).Nonempty := ⟨_, mem_image_of_mem _ (hfs _ trivial), hI⟩

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
h : I.piecewise f g ∈ v
S : Set ((a : ι) → X a) := update (I.piecewise f g) i '' s i
hsub : S ⊆ univ.pi s
hconn : IsPreconnected S
hSu : (S ∩ u).Nonempty
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di : IsDenseInducing i
s : Set α
⊢ Dense (i '' s) ↔ Dense s

Tactic:
refine ⟨fun H x => ?_, di.dense.dense_image di.continuous⟩
  rw [di.isInducing.closure_eq_preimage_closure_image, H.closure_eq, preimage_univ]
  trivial

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
⊢ ContinuousAt φ b

Tactic:
suffices ∀ V' ∈ 𝓝 (φ b), IsClosed V' → φ ⁻¹' V' ∈ 𝓝 b by
    simpa [ContinuousAt, (closed_nhds_basis (φ b)).tendsto_right_iff]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
⊢ ∀ V' ∈ 𝓝 (φ b), IsClosed[inst✝¹] V' → φ ⁻¹' V' ∈ 𝓝 b
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ IsLindelof s ↔ IsLindelof (f '' s)

Tactic:
refine ⟨fun hs => hs.image hf.continuous, fun hs F F_ne_bot _ F_le => ?_⟩

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
hs : IsLindelof (f '' s)
F : Filter X
F_ne_bot : F.NeBot
x✝ : CountableInterFilter F
F_le : F ≤ 𝓟 s
⊢ ∃ x ∈ s, ClusterPt x F
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
h : IsNowhereDense s
⊢ IsNowhereDense (f '' s)

Tactic:
rw [isNowhereDense_iff_forall_notMem_nhds, forall_mem_image] at *
  simp_rw [hf.nhds_eq_comap, hf.closure_eq_preimage_closure_image] at h
  exact fun x x_mem hx ↦ h x x_mem (preimage_mem_comap hx)

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
S : Set α
hS : IsPreconnected S
h : IsDiscrete S
⊢ S.Subsingleton

Tactic:
by
    have : DiscreteTopology S := isDiscrete_iff_discreteTopology.mp h
    have : PreconnectedSpace S := isPreconnected_iff_preconnectedSpace.mp hS
    have : Subsingleton S := subsingleton_of_preconnected_totallyDisconnected
    simpa using this

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

Goal state before:
pp: case h
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
S : Set (Set X)
hS : ∀ t ∈ S, IsNowhereDense t
hc : S.Countable
hsub : s ⊆ ⋃₀ S
⊢ (∀ ⦃x : Set X⦄, x ∈ S → IsClosed[inst✝] (closure[inst✝] x) ∧ IsNowhereDense (closure[inst✝] x)) ∧
    (compl '' closure[inst✝] '' S).Countable ∧ s ⊆ ⋃₀ (closure[inst✝] '' S)

Tactic:
exact ⟨fun s hs ↦ ⟨isClosed_closure, (hS s hs).closure⟩,
      (hc.image _).image _, hsub.trans (sUnion_mono_subsets fun s ↦ subset_closure)⟩

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace] ⇑(Fin.appendEquiv m n)

Tactic:
Fin.appendEquiv_eq_homeomorph

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace]
    ⇑(sumArrowHomeomorphProdArrow.symm.trans (piCongrLeft finSumFinEquiv)).toEquiv
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
p : ι → Prop
Y : ι → Type u_8
inst✝¹ : (i : ι) → TopologicalSpace (Y i)
inst✝ : DecidablePred p
j : ι
⊢ Continuous[instTopologicalSpaceProd, inst✝¹ j] fun a ↦ (Equiv.piEquivPiSubtypeProd p Y).invFun a j

Tactic:
dsimp only [Equiv.piEquivPiSubtypeProd]; split_ifs
      exacts [(continuous_apply _).comp continuous_fst, (continuous_apply _).comp continuous_snd]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsHomeomorph f ↔ IsQuotientMap f ∧ Injective f

Tactic:
refine ⟨fun h ↦ ⟨h.isQuotientMap, h.injective⟩,
    fun h ↦ ⟨h.1.continuous, fun s hs ↦ ?_, h.2, h.1.surjective⟩⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsQuotientMap f ∧ Injective f
s : Set X
hs : IsOpen[inst✝¹] s
⊢ IsOpen[inst✝] (f '' s)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
hf : Cauchy f
adhs : ClusterPt x f
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ s
⊢ ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t

Tactic:
use t, t_mem, ht

Goal state after:
case right
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
hf : Cauchy f
adhs : ClusterPt x f
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ s
⊢ ∃ y, (x, y) ∈ s ∧ y ∈ t
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
⊢ ∃ r ∈ 𝓤 α, IsClosed[instTopologicalSpaceProd] r ∧ r ⊆ t

Tactic:
rcases comp_comp_symm_mem_uniformity_sets h with ⟨w, w_in, w_symm, r⟩

Goal state after:
α : Type ua
inst✝ : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
r : w ○ w ○ w ⊆ t
⊢ ∃ r ∈ 𝓤 α, IsClosed[instTopologicalSpaceProd] r ∧ r ⊆ t