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

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
S : Set Y
⊢ DiscreteTopology ↑S ↔ ∀ y ∈ S, ∃ U, IsOpen[inst✝] U ∧ U ∩ S = {y}

Tactic:
by
  simp [discreteTopology_iff_isOpen_singleton, isOpen_induced_iff, Set.ext_iff]
  grind

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
inst✝ : IndiscreteTopology X
u v : Set X
⊢ IsOpen[inst✝²] u → IsOpen[inst✝²] v → (univ ∩ u).Nonempty → (univ ∩ v).Nonempty → (univ ∩ (u ∩ v)).Nonempty

Tactic:
by
    simp only [IndiscreteTopology.isOpen_iff, univ_inter]
    rintro ⟨h | h⟩ <;> simp_all

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
π : X → Y
h : IsOpenQuotientMap (Prod.map π π)
⊢ IsClosed[instTopologicalSpaceProd] (diagonal Y) ↔ IsClosed[instTopologicalSpaceProd] {q | π q.1 = π q.2}

Tactic:
refine ⟨fun H ↦ H.preimage h.continuous, fun H ↦ ?_⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
π : X → Y
h : IsOpenQuotientMap (Prod.map π π)
H : IsClosed[instTopologicalSpaceProd] {q | π q.1 = π q.2}
⊢ IsClosed[instTopologicalSpaceProd] (diagonal Y)
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case h₂
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ Z ⊆ closure[inst✝] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ

Tactic:
· rw [← Set.inter_eq_right.mpr h]
    apply subset_closure_inter_of_isPreirreducible_of_isOpen hZ.1.2
    · rw [Set.sUnion_eq_biUnion, isOpen_compl_iff]
      exact hX.sdiff.isClosed_biUnion fun W hW ↦ isClosed_of_mem_irreducibleComponents W hW.1
    · rw [Set.inter_compl_nonempty_iff]
      exact mt (mem_of_subset_sUnion_irreducibleComponents Z hZ _ hX.sdiff Set.sdiff_subset)
        (Set.notMem_sdiff_of_mem (Set.mem_singleton Z))

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

Goal state before:
pp: case inr
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst✝] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst✝] {x}) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
H : T1Space X
s : Set (CofiniteTopology X)
hs : sᶜ.Finite
⊢ IsOpen[inst✝] (⇑CofiniteTopology.of ⁻¹' sᶜ)ᶜ

Tactic:
exact hs.preimage (Equiv.injective _).injOn |>.isClosed.isOpen_compl

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

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

Tactic:
intro m

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
a : α
⊢ 𝓝[univ] a = 𝓝 a

Tactic:
nhdsWithin_univ

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
a : α
⊢ 𝓝 a = 𝓝 a
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space X
x : X
s : Set X
f : X → Y
⊢ ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f s x

pp: case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space X
x y : X
s : Set X
f : X → Y
h : x ≠ y
⊢ ContinuousWithinAt f (insert y s) x ↔ ContinuousWithinAt f s x

Tactic:
· exact continuousWithinAt_insert_self

Goal state after:
case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space X
x y : X
s : Set X
f : X → Y
h : x ≠ y
⊢ ContinuousWithinAt f (insert y s) x ↔ ContinuousWithinAt f s x
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space X
x y : X
s : Set X
f : X → Y
⊢ ContinuousWithinAt f (insert ?m.22 (s \ {y})) x ↔ ContinuousWithinAt f s x

pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space X
x y : X
s : Set X
f : X → Y
⊢ X

Tactic:
insert_sdiff_singleton,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space X
x y : X
s : Set X
f : X → Y
⊢ ContinuousWithinAt f (insert y s) x ↔ ContinuousWithinAt f s x
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
⊢ IsPreconnected (⋃ n ∈ t, s n)

Tactic:
let R := fun i j : ι => (s i ∩ s j).Nonempty ∧ i ∈ t

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
⊢ IsPreconnected (⋃ n ∈ t, s n)
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, U ↑x ⋯

Tactic:
have := hs.elim_countable_subcover (fun x : s ↦ interior (U x x.2)) (fun _ ↦ isOpen_interior)
    fun x hx ↦
      mem_iUnion.2 ⟨⟨x, hx⟩, mem_interior_iff_mem_nhds.2 <| hU _ _⟩
  rcases this with ⟨r, ⟨hr, hs⟩⟩
  use r, hr
  apply Subset.trans hs
  apply iUnion₂_subset
  intro i hi
  apply Subset.trans interior_subset
  exact subset_iUnion_of_subset i (subset_iUnion_of_subset hi (Subset.refl _))

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
x : X
s : Set X
h : s ∈ 𝓝 x
⊢ ∃ t ∈ 𝓝 x, IsClosed[inst✝¹] t ∧ t ⊆ s

Tactic:
have h' := (regularSpace_TFAE X).out 0 3

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
x : X
s : Set X
h : s ∈ 𝓝 x
h' : RegularSpace X ↔ ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst✝¹] t ∧ t ⊆ s
⊢ ∃ t ∈ 𝓝 x, IsClosed[inst✝¹] t ∧ t ⊆ s
Module: Mathlib.Topology.Connected.Basic

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

Tactic:
by
  simp_rw [← connectedComponentIn_nonempty_iff, IsConnected, isPreconnected_connectedComponentIn,
    and_true]

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
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed[inst✝¹] V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen[inst✝²] V₂
hV₂ : ∀ x ∈ i ⁻¹' V₂, f x ∈ V'
this : ∀ x ∈ V₁ ∩ V₂, φ x ∈ V'
⊢ φ ⁻¹' V' ∈ 𝓝 b

Tactic:
by filter_upwards [inter_mem V₁_in V₂_in] using this

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst✝] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : ℕ → Set X := fun n ↦ p '' f n ∪ (closure[inst✝²] s)ᶜ
⊢ Dense (⋂ n, f n)

Tactic:
have c_open (n : ℕ) : IsOpen (c n) := IsOpen.union (hp.isOpenMap (f n) (hof n))
    isClosed_closure.isOpen_compl

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst✝] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : ℕ → Set X := fun n ↦ p '' f n ∪ (closure[inst✝²] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
⊢ Dense (⋂ n, f n)
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst✝] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : ℕ → Set X := fun n ↦ p '' f n ∪ (closure[inst✝²] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
n : ℕ
⊢ closure[inst✝²] (c n) ⊆ univ ∧ univ ⊆ closure[inst✝²] (c n)

Tactic:
have : univ ⊆ closure (c n) := calc
      _ ⊆ (interior (closure s)) ∪ (interior (closure s))ᶜ := by grind
      _ ⊆ closure s ∪ (interior (closure s))ᶜ := by gcongr; exact interior_subset
      _ ⊆ closure (p '' f n) ∪ (interior (closure s))ᶜ := union_subset_union
          (closure_minimal (hp.continuous.range_subset_closure_image_dense (hdf n))
          isClosed_closure) (subset_refl (interior (closure s))ᶜ)
      _ ⊆ closure (p '' f n) ∪ closure ((closure s)ᶜ) := union_subset_union (by simp) (by simp)
      _ = closure (c n) := closure_union.symm

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst✝] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : ℕ → Set X := fun n ↦ p '' f n ∪ (closure[inst✝²] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
n : ℕ
this : univ ⊆ closure[inst✝²] (c n)
⊢ closure[inst✝²] (c n) ⊆ univ ∧ univ ⊆ closure[inst✝²] (c n)
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X ≃ Y
⊢ IsHomeomorph ⇑e ↔ Continuous[inst✝¹, inst✝] ⇑e ∧ IsOpenMap ⇑e

Tactic:
exact ⟨fun h ↦ ⟨h.continuous, h.isOpenMap⟩, fun ⟨hc, ho⟩ ↦ ⟨hc, ho, e.bijective⟩⟩

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y | ∃ x ∈ s, (x, y) ∈ r}
g : ↑u → α
hgs : ∀ (x : ↑u), g x ∈ s
hgr : ∀ (x : ↑u), (g x, ↑x) ∈ r
⊢ ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f

Tactic:
refine ⟨range g, ?_, ?_, ?_⟩

Goal state after:
case refine_1
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y | ∃ x ∈ s, (x, y) ∈ r}
g : ↑u → α
hgs : ∀ (x : ↑u), g x ∈ s
hgr : ∀ (x : ↑u), (g x, ↑x) ∈ r
⊢ range g ⊆ s

case refine_2
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y | ∃ x ∈ s, (x, y) ∈ r}
g : ↑u → α
hgs : ∀ (x : ↑u), g x ∈ s
hgr : ∀ (x : ↑u), (g x, ↑x) ∈ r
⊢ (range g).Finite

case refine_3
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y | ∃ x ∈ s, (x, y) ∈ r}
g : ↑u → α
hgs : ∀ (x : ↑u), g x ∈ s
hgr : ∀ (x : ↑u), (g x, ↑x) ∈ r
⊢ U.preimage (range g) ∈ f
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst✝ : Finite ι
f : ι → Filter α
h : ∀ (i : ι), (f i).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
t : ι → Set α
htf : ∀ (x : ι), (t x).Finite
ht : ∀ (x : ι), U.preimage (t x) ∈ f x
⊢ U.preimage (⋃ i, t i) ∈ ⨆ i, f i

Tactic:
U.preimage_iUnion,

Goal state after:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst✝ : Finite ι
f : ι → Filter α
h : ∀ (i : ι), (f i).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
t : ι → Set α
htf : ∀ (x : ι), (t x).Finite
ht : ∀ (x : ι), U.preimage (t x) ∈ f x
⊢ ⋃ i, U.preimage (t i) ∈ ⨆ i, f i
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
⊢ ∀ (y : ℕ), s y ∈ ⋃ y ∈ {k | k ≤ n}, {x | (x, s y) ∈ a}

Tactic:
intro m

Goal state after:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
m : ℕ
⊢ s m ∈ ⋃ y ∈ {k | k ≤ n}, {x | (x, s y) ∈ a}
Module: Mathlib.Topology.UniformSpace.Pi

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
β : Type u_3
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝¹ : UniformSpace β
inst✝ : ∀ (i : ι), CompleteSpace (α i)
f : Filter ((i : ι) → α i)
this : f.NeBot
hf : ∀ (i : ι), ∃ x, map (eval i) f ≤ 𝓝 x
⊢ ∃ x, f ≤ 𝓝 x

Tactic:
choose x hx using hf

Goal state after:
ι : Type u_1
ι' : Type u_2
β : Type u_3
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝¹ : UniformSpace β
inst✝ : ∀ (i : ι), CompleteSpace (α i)
f : Filter ((i : ι) → α i)
this : f.NeBot
x : (i : ι) → α i
hx : ∀ (i : ι), map (eval i) f ≤ 𝓝 (x i)
⊢ ∃ x, f ≤ 𝓝 x
Module: Mathlib.Topology.UniformSpace.UniformApproximation

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoLocallyUniformlyOn F f p s
hc : ∃ᶠ (n : ι) in p, ContinuousOn (F n) s
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set α
ht : t ∈ 𝓝[s] x
H : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
n : ι
hFc : ContinuousOn (F n) s
hF : ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u

Tactic:
exact ⟨t, ht, ⟨F n, hFc.continuousWithinAt hx, hF⟩⟩

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

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
⊢ (∀ U ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[univ] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U) ↔
    ∀ U ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U

Tactic:
nhdsWithin_univ

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
⊢ (∀ U ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U) ↔
    ∀ U ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
⊢ (∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[univ] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U) ↔
    ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
nhdsWithin_univ

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
⊢ map (fun p ↦ m p.1 p.2) (f ×ˢ g) = map₂ m f g

Tactic:
rw [map₂, copy_eq, uncurry_def]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
S : Set β
hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p s
⊢ UniformEquicontinuousOn F S ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
by
  rw [uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn,
    hβ.tendsto_iff (UniformFun.hasBasis_uniformity ι α)]
  simp only [Prod.forall]
  rfl

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
⊢ UniformContinuous fun x ↦ (f x)⁻¹

Tactic:
have : UniformContinuous fun x => 1 / f x := uniformContinuous_const.div hf
  simp_all

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
dr : β × β → β := fun xy ↦ xy.2 * xy.1⁻¹
dl : β × β → β := fun xy ↦ xy.1⁻¹ * xy.2
⊢ comap (fun gx ↦ gx.1 * gx.2 * gx.1⁻¹) (𝓝 1) = comap snd (𝓝 1)

Tactic:
let conj : β × β → β := fun gx ↦ gx.1 * gx.2 * gx.1⁻¹

Goal state after:
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
dr : β × β → β := fun xy ↦ xy.2 * xy.1⁻¹
dl : β × β → β := fun xy ↦ xy.1⁻¹ * xy.2
conj : β × β → β := fun gx ↦ gx.1 * gx.2 * gx.1⁻¹
⊢ comap (fun gx ↦ gx.1 * gx.2 * gx.1⁻¹) (𝓝 1) = comap snd (𝓝 1)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
α : Type u_1
l : Filter α
inst✝¹ : l.NeBot
inst✝ : T2Space G
f g : α → G
a b : G
hf : Tendsto f l (𝓝 a)
hg : Tendsto g l (𝓝 b)
h : a = b
⊢ Tendsto (fun x ↦ f x / g x) l (𝓝 1)

Tactic:
by subst h; simpa using hf.div' hg

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsClosed[inst✝²] {1}
x : G
⊢ IsClosed[inst✝²] {x}

Tactic:
simpa using isClosedMap_mul_right x _ h

Goal state after:
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' Ico a b = Ico (update f i a) (update f i b)

Tactic:
by
  rw [← Icc_sdiff_right, ← Icc_sdiff_right, image_sdiff (update_injective _ _), image_singleton,
    image_update_Icc]

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

Goal state before:
pp: α : Type u
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ (⨅ j, ⨅ (_ : a ∈ Ioi j), 𝓟 (Ioi j)) ⊓ ⨅ j, ⨅ (_ : a ∈ Iio j), 𝓟 (Iio j) =
    (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)

Tactic:
mem_Ioi,

Goal state after:
α : Type u
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ (⨅ j, ⨅ (_ : j < a), 𝓟 (Ioi j)) ⊓ ⨅ j, ⨅ (_ : a ∈ Iio j), 𝓟 (Iio j) =
    (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b, ⨅ (_ : a < b), 𝓟 (Iio b)
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ toIocDiv hp a =ᶠ[𝓝[≤] x] fun x_1 ↦ toIocDiv hp a x

Tactic:
simp only [Filter.EventuallyEq, toIocDiv_eq_iff, sub_mem_Ioc_iff_left]
  apply Ioc_mem_nhdsLE_of_mem
  rw [← sub_mem_Ioc_iff_left, ← toIocDiv_eq_iff]

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

Goal state before:
pp: case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl✝ : ∃ l, l < a
hu✝ : ∃ u, a < u
h : s ∈ 𝓝 a
u : α
au : a < u
hu : Ico a u ⊆ s
l : α
la : l < a
hl : Ioc l a ⊆ s
⊢ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s

Tactic:
exact ⟨l, u, ⟨la, au⟩, Ioc_union_Ico_eq_Ioo la au ▸ union_subset hl hu⟩

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
H : ∀ (a : Set α), IsOpen[inst✝³] a → {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a}.Countable
x : α
hx : x ∈ s
⊢ x ∈ ⋃ a ∈ countableBasis α, {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a}

Tactic:
rcases (isBasis_countableBasis α).exists_mem_of_ne (hy x hx).ne with ⟨a, ab, xa, ya⟩

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
H : ∀ (a : Set α), IsOpen[inst✝³] a → {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a}.Countable
x : α
hx : x ∈ s
a : Set α
ab : a ∈ countableBasis α
xa : x ∈ a
ya : y x ∉ a
⊢ x ∈ ⋃ a ∈ countableBasis α, {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a}
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
this : ∀ (x : ↑{x | n • x = 0}), ∃ k y, ↑y = ↑x ∧ n • y = ↑k • p
⊢ {x | n • x = 0}.encard ≤ ↑n

Tactic:
choose f hf using this

Goal state after:
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
f : ↑{x | n • x = 0} → Fin n
hf : ∀ (x : ↑{x | n • x = 0}), ∃ y, ↑y = ↑x ∧ n • y = ↑(f x) • p
⊢ {x | n • x = 0}.encard ≤ ↑n
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : Mono (homologyMap φ)
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A ⟶ S₂.X₁
fac : x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f

pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 → ∀ (y₁ : A ⟶ S₂.X₁), x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f
⊢ Mono (homologyMap φ)

Tactic:
· suffices S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ = 0 by
      rwa [← S₁.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements]
    simp only [← cancel_mono (homologyMap φ), zero_comp, assoc,
      homologyπ_naturality, liftCycles_comp_cyclesMap_assoc,
      S₂.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements]
    exact ⟨A, 𝟙 A, inferInstance, y₁, by simpa using fac⟩

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 → ∀ (y₁ : A ⟶ S₂.X₁), x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f
⊢ Mono (homologyMap φ)
Module: Mathlib.CategoryTheory.Monad.Equalizer

Goal state before:
pp: case refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
⊢ ∀ {m : s.pt ⟶ (beckCoalgebraFork X).pt}, m ≫ (beckCoalgebraFork X).ι = s.ι → m = { f := s.ι.f ≫ T.ε.app X.A, h := ⋯ }

Tactic:
intro m

Goal state after:
case refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
m : s.pt ⟶ (beckCoalgebraFork X).pt
⊢ m ≫ (beckCoalgebraFork X).ι = s.ι → m = { f := s.ι.f ≫ T.ε.app X.A, h := ⋯ }