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

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

Tactic:
rw [hg]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht✝ : t ∈ iInf f
i✝ : ι
s₁✝ s₂✝ : Set α
hs : s₁✝ ∈ f i✝
ht : ⨅ i, (f i).lift g ≤ g s₂✝
⊢ ⨅ i, (f i).lift g ≤ g s₁✝ ⊓ g s₂✝
Module: Mathlib.Order.Filter.Lift

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

Tactic:
cases isEmpty_or_nonempty ι
  · simp [iInf_of_empty, hg']
  · exact lift_iInf hg

Goal state after:
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 : α
⊢ toIcoMod hp (a + p) b = toIcoMod hp a b + p

Tactic:
by
  simpa only [one_zsmul] using toIcoMod_add_zsmul' hp a b 1

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsOpen s ↔ ∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t

Tactic:
rw [← subset_interior_iff_isOpen]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ s ⊆ interior s ↔ ∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t
Module: Mathlib.Topology.Closure

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

Tactic:
simp [closure_eq_compl_interior_compl, compl_inter]

Goal state after:
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
B : interior (frontier s) ⊆ interior s
C : interior (frontier s) ⊆ frontier s
⊢ interior (frontier s) ⊆ s \ interior s

Tactic:
by simpa [A] using C

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ : α
h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₃₁ : x₃' ≤ x₁ + p
⊢ x₁ + p ≤ x₂' + p

Tactic:
simp [x₂', left_le_toIcoMod]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s₁ s₂ : Set X
h : 𝓝 x ⊓ 𝓟 s₁ ⊔ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
h₁ : s₁ᶜ ∈ 𝓝 x
⊢ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥

Tactic:
inf_principal_eq_bot.mpr h₁,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
s₁ s₂ : Set X
h : ⊥ ⊔ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
h₁ : s₁ᶜ ∈ 𝓝 x
⊢ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
Module: Mathlib.Topology.Maps.Basic

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

Tactic:
rw [isInducing_iff, hg.eq_induced, induced_compose, h.eq_induced]

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
⊢ IsCoinducing f ∧ Surjective f ↔ Surjective f ∧ ∀ (s : Set Y), IsClosed[inst✝] s ↔ IsClosed[inst✝¹] (f ⁻¹' s)

Tactic:
isCoinducing_iff_isClosed,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ (∀ (s : Set Y), IsClosed[inst✝¹] (f ⁻¹' s) ↔ IsClosed[inst✝] s) ∧ Surjective f ↔
    Surjective f ∧ ∀ (s : Set Y), IsClosed[inst✝] s ↔ IsClosed[inst✝¹] (f ⁻¹' s)
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
⊢ IsClosedMap f ↔ ∀ {s : Set Y}, ∀ x ∈ 𝓝ˢ (f ⁻¹' s), x ∈ comap f (𝓝ˢ s)

Tactic:
mem_comap'',

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsClosedMap f ↔ ∀ {s : Set Y}, ∀ x ∈ 𝓝ˢ (f ⁻¹' s), kernImage f x ∈ 𝓝ˢ s
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ (𝓝 a ⊓ 𝓟 (s ∩ t))

Tactic:
← inf_assoc,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓝 a ⊓ 𝓟 (s ∩ t)
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
h : t ∈ 𝓝[s] a
⊢ 𝓝[s ∩ t] a = 𝓝[s] a

Tactic:
by
  rw [inter_comm, nhdsWithin_inter_of_mem h]

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

Goal state before:
pp: case inr.mp
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
⊢ IsOpen[instTopologicalSpaceProd] (s ×ˢ t) → IsOpen[inst✝¹] s ∧ IsOpen[inst✝] t ∨ s = ∅ ∨ t = ∅

Tactic:
intro (H : IsOpen (s ×ˢ t))

Goal state after:
case inr.mp
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 ∧ IsOpen[inst✝] t ∨ s = ∅ ∨ t = ∅
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:
rw [interior_inter, hs.interior_eq]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable ↑(t i)
a✝ : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : ↥I) → ↑(t ↑i)) → (i : ι) → X i :=
  fun x i ↦
    match x with
    | ⟨I, g⟩ => if hi : i ∈ I then ↑(g ⟨i, hi⟩) else default i
U : Set ((i : ι) → X i)
hU : IsOpen[Pi.topologicalSpace] U
x✝ : U.Nonempty
g : (i : ι) → X i
hg : g ∈ U
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst✝² a] (u a) ∧ g a ∈ u a
huU : (↑I).pi u ⊆ U
y : (i : ↥I) → X ↑i
hyt : ∀ (i : ↥I), y i ∈ t ↑i
hyu : ∀ (i : ↥I), y i ∈ u ↑i
⊢ (U ∩ range f).Nonempty

Tactic:
lift y to ∀ i : I, t i using hyt

Goal state after:
α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable ↑(t i)
a✝ : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : ↥I) → ↑(t ↑i)) → (i : ι) → X i :=
  fun x i ↦
    match x with
    | ⟨I, g⟩ => if hi : i ∈ I then ↑(g ⟨i, hi⟩) else default i
U : Set ((i : ι) → X i)
hU : IsOpen[Pi.topologicalSpace] U
x✝ : U.Nonempty
g : (i : ι) → X i
hg : g ∈ U
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst✝² a] (u a) ∧ g a ∈ u a
huU : (↑I).pi u ⊆ U
y : (i : ↥I) → ↑(t ↑i)
hyu : ∀ (i : ↥I), (fun i ↦ ↑(y i)) i ∈ u ↑i
⊢ (U ∩ range f).Nonempty
Module: Mathlib.Topology.Bornology.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Bornology α
s : Set ι
f : ι → Set α
hs : s.Finite
⊢ IsBounded (⋃ i ∈ s, f i) ↔ ∀ i ∈ s, IsBounded (f i)

Tactic:
by
  simp only [← isCobounded_compl_iff, compl_iUnion, isCobounded_biInter hs]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s✝ : Set α
inst✝² : TopologicalSpace β
inst✝¹ : SeparableSpace α
inst✝ : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
t : Set β
htc : t.Countable
htd : Dense t
⊢ SeparableSpace (α ⊕ β)

Tactic:
refine ⟨Sum.inl '' s ∪ Sum.inr '' t, (hsc.image _).union (htc.image _), ?_⟩

Goal state after:
α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s✝ : Set α
inst✝² : TopologicalSpace β
inst✝¹ : SeparableSpace α
inst✝ : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
t : Set β
htc : t.Countable
htd : Dense t
⊢ Dense (Sum.inl '' s ∪ Sum.inr '' t)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen[inst✝ i] s
⊢ IsOpen[instTopologicalSpaceSigma] (Sigma.mk i '' s)

Tactic:
rw [isOpen_sigma_iff]

Goal state after:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen[inst✝ i] s
⊢ ∀ (i_1 : ι), IsOpen[inst✝ i_1] (Sigma.mk i_1 ⁻¹' Sigma.mk i '' s)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : 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'
u : Set α
hu : u ∈ s'
⊢ ∃ f, f.Finite ∧ f ⊆ t ∧ ⋂₀ f = u

Tactic:
by simpa [t', and_assoc] using s't' hu

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
x : X
U : Set X
hU : IsOpen[inst✝¹] U
hx : x ∈ U
⊢ ∃ K, IsCompact K ∧ x ∈ interior K ∧ K ⊆ U

Tactic:
by
  rcases LocallyCompactSpace.local_compact_nhds x U (hU.mem_nhds hx) with ⟨K, h1K, h2K, h3K⟩
  exact ⟨K, h3K, mem_interior_iff_mem_nhds.2 h1K, h2K⟩

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst✝¹] U
hZ : IsClosed[inst✝¹] Z
hUZ : range f = U ∩ Z
x : X
H : U ∈ 𝓝 (f x)
⊢ (𝓝 x).HasBasis (fun s ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun s ↦ f ⁻¹' (s ∩ Z)

Tactic:
rw [hf.nhds_eq_comap, ← comap_nhdsWithin_range, hUZ,
      nhdsWithin_inter_of_mem (nhdsWithin_le_nhds H)]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst✝¹] U
hZ : IsClosed[inst✝¹] Z
hUZ : range f = U ∩ Z
x : X
H : U ∈ 𝓝 (f x)
⊢ (comap f (𝓝[Z] f x)).HasBasis (fun s ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun s ↦ f ⁻¹' (s ∩ Z)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
⊢ comap f (cocompact Y) ≤ cocompact X

Tactic:
rw [(Filter.hasBasis_cocompact.comap f).le_basis_iff Filter.hasBasis_cocompact]
  intro t ht
  refine ⟨f '' t, ht.image hf, ?_⟩
  simpa using t.subset_preimage_image f

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:

Tactic:
pure (f x)
    _ = map f (pure x) := (map_pure f x).symm
    _ ≤ map f (𝓝 y ⊓ 𝓟 s) := map_mono (le_inf h ((pure_le_principal x).mpr hx))
    _ = map f (𝓝[s] y) := rfl
    _ ≤ _ := hf.tendsto

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: α : Type u_4
inst✝ : TopologicalSpace α
⊢ Nontrivial (SeparationQuotient α) ↔ NontrivialTopology α

Tactic:
simpa [not_subsingleton_iff_nontrivial] using subsingleton_iff.not

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ map mk (𝓝 x) = 𝓝 (mk x)

Tactic:
← comap_mk_nhds_mk,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ map mk (comap mk (𝓝 (mk x))) = 𝓝 (mk x)
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
s : Set (SeparationQuotient X × SeparationQuotient Y)
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf)) (map (Prod.map mk mk) (𝓝 (x, y) ⊓ comap (Prod.map mk mk) (𝓟 s))) l ↔
    Tendsto (uncurry f) (𝓝[Prod.map mk mk ⁻¹' s] (x, y)) l

Tactic:
comap_principal

Goal state after:
X : Type u_1
Y : Type u_2
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
s : Set (SeparationQuotient X × SeparationQuotient Y)
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf)) (map (Prod.map mk mk) (𝓝 (x, y) ⊓ 𝓟 (Prod.map mk mk ⁻¹' s))) l ↔
    Tendsto (uncurry f) (𝓝[Prod.map mk mk ⁻¹' s] (x, y)) l
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
U s : Set X
hU : ∃ u, IsOpen[inst✝¹] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U
hs : Finite ↑s
⊢ ∃ u, IsOpen[inst✝¹] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U \ s

Tactic:
obtain ⟨t, ht, h₁ts, h₂ts⟩ := hU

Goal state after:
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
U s : Set X
hs : Finite ↑s
t : Set X
ht : IsOpen[inst✝¹] t
h₁ts : x ∈ t
h₂ts : t ∩ {x}ᶜ ⊆ U
⊢ ∃ u, IsOpen[inst✝¹] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U \ s
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
S : Set X
⊢ (∀ x ∈ S, S ⊆ closure[inst✝¹] {x}) → IsPreirreducible S

Tactic:
intro h u v hu hv ⟨x, hxs, hxu⟩ ⟨y, hys, hyv⟩

Goal state after:
case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
S : Set X
h : ∀ x ∈ S, S ⊆ closure[inst✝¹] {x}
u v : Set X
hu : IsOpen[inst✝¹] u
hv : IsOpen[inst✝¹] v
x : X
hxs : x ∈ S
hxu : x ∈ u
y : X
hys : y ∈ S
hyv : y ∈ v
⊢ (S ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case neg
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
x y : X
hTd : ∀ t ∈ T, ¬Disjoint (𝓝 x) (𝓝 y)
⊢ ⨅ t ∈ T, 𝓝 x ≤ ⨅ t ∈ T, 𝓝 y ∨ Disjoint (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)

Tactic:
exact .inl <| iInf₂_mono fun t ht ↦ ((hT t ht).1 x y).resolve_right (hTd t ht)

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

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β✝ : Type u_3
l✝ : Filter α✝
inst✝² : CountableInterFilter l✝
α : Type u_4
β : Type u_5
l : Filter α
m : Filter β
inst✝¹ : CountableInterFilter l
inst✝ : CountableInterFilter m
S : Set (Set (α × β))
⊢ S.Countable → (∀ s ∈ S, s ∈ l.curry m) → ⋂₀ S ∈ l.curry m

Tactic:
Sct

Goal state after:
ι : Sort u_1
α✝ : Type u_2
β✝ : Type u_3
l✝ : Filter α✝
inst✝² : CountableInterFilter l✝
α : Type u_4
β : Type u_5
l : Filter α
m : Filter β
inst✝¹ : CountableInterFilter l
inst✝ : CountableInterFilter m
S : Set (Set (α × β))
Sct : S.Countable
⊢ (∀ s ∈ S, s ∈ l.curry m) → ⋂₀ S ∈ l.curry m
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed[inst✝] t
⊢ IsLindelof (s ∩ t)

Tactic:
by
  intro f hnf _ hstf
  rw [← inf_principal, le_inf_iff] at hstf
  obtain ⟨x, hsx, hx⟩ : ∃ x ∈ s, ClusterPt x f := hs hstf.1
  have hxt : x ∈ t := ht.mem_of_nhdsWithin_neBot <| hx.mono hstf.2
  exact ⟨x, ⟨hsx, hxt⟩, hx⟩

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝] (t i)
hst : s ∩ ⋂ i, t i = ∅
U : ι → Set X := tᶜ
⊢ ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅

Tactic:
have hUo : ∀ i, IsOpen (U i) := by simp only [U, Pi.compl_apply, isOpen_compl_iff]; exact htc

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝] (t i)
hst : s ∩ ⋂ i, t i = ∅
U : ι → Set X := tᶜ
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
⊢ ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 :
  IsClosed[inst✝] (u ∩ s) →
    IsClosed[inst✝] (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∩ s ∨ s ⊆ v ∩ s
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
subset_inter_iff,

Goal state after:
case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 :
  IsClosed[inst✝] (u ∩ s) →
    IsClosed[inst✝] (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∧ s ⊆ s ∨ s ⊆ v ∩ s
⊢ s ⊆ u ∨ s ⊆ v
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
h : PreconnectedSpace α
x : α
⊢ connectedComponent x = univ

Tactic:
exact eq_univ_of_univ_subset <| isPreconnected_univ.subset_connectedComponent (mem_univ x)

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

Goal state before:
pp: X : Type u
Y : Type v
ι : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t✝ : Set X
inst✝ : SecondCountableTopology X
t : Set X
x✝¹ : t ⊆ univ
x✝ : Filter X
⊢ ∀ [x✝.NeBot] [CountableInterFilter x✝], x✝ ≤ 𝓟 t → ∃ x ∈ t, ClusterPt x x✝

Tactic:
apply isLindelof_iff_countable_subcover.mpr
    intro ι U hι hcover
    have := @isOpen_iUnion_countable X _ _ ι U hι
    rcases this with ⟨t, ⟨htc, htu⟩⟩
    use t, htc
    exact subset_of_subset_of_eq hcover (id htu.symm)

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
T : Set (Set X)
To : ∀ t ∈ T, IsOpen[inst✝] t
Tct : T.Countable
hd : Dense (⋂₀ T)
⊢ ⋂₀ T ∈ residual X

Tactic:
exact
    (countable_sInter_mem Tct).mpr fun t tT =>
      residual_of_dense_open (To t tT) (hd.mono (sInter_subset_of_mem tT))

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 ↔ Continuous[inst✝¹, inst✝] f ∧ ∃ g, LeftInverse g f ∧ RightInverse g f ∧ Continuous[inst✝, inst✝¹] g

Tactic:
by
  refine ⟨fun hf ↦ ⟨hf.continuous, ?_⟩, fun ⟨hf, g, hg⟩ ↦ ?_⟩
  · let h := hf.homeomorph f
    exact ⟨h.symm, h.left_inv, h.right_inv, h.continuous_invFun⟩
  · exact (Homeomorph.mk ⟨f, g, hg.1, hg.2.1⟩ hf hg.2.2).isHomeomorph

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
f : ℕ ≃ ℕ
H : CauchySeq (u ∘ ⇑f)
⊢ CauchySeq u

Tactic:
simpa only [Function.comp_def, f.apply_symm_apply] using H.comp_injective f.symm.injective

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

Goal state before:
pp: case hh
α : Type ua
inst✝ : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
x✝ : α × α
x y : α
hp : (x, y) ∈ s
⊢ Monotone fun s ↦ {y | (y, x) ∈ s} ×ˢ {y_1 | (y, y_1) ∈ s}

Tactic:
exact fun _ _ h _ h' => ⟨h h'.1, h h'.2⟩

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s : Set α
⊢ IsComplete s ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x ∈ s, ↑l ≤ 𝓝 x

Tactic:
by
  refine ⟨fun h l => h l, fun H => isComplete_iff_clusterPt.2 fun l hl hls => ?_⟩
  have := hl.1
  rcases H (Ultrafilter.of l) hl.ultrafilter_of ((Ultrafilter.of_le l).trans hls) with ⟨x, hxs, hxl⟩
  exact ⟨x, hxs, (ClusterPt.of_le_nhds hxl).mono (Ultrafilter.of_le l)⟩

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}

Tactic:
← Filter.totallyBounded_principal_iff

Goal state after:
α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : (𝓟 s).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
ι : Sort u_1
ι' : Sort u_2
p : ι → Prop
p' : ι' → Prop
s : ι → Set (α × α)
s' : ι' → Set (β × β)
h : (𝓤 α).HasBasis p s
h' : (𝓤 β).HasBasis p' s'
f : α → β
⊢ IsUniformEmbedding f ↔
    Injective f ∧
      (∀ (i : ι'), p' i → ∃ j, p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
        ∀ (j : ι), p j → ∃ i, p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j

Tactic:
by
  rw [isUniformEmbedding_iff, and_comm, h.isUniformInducing_iff h']

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝¹ : CompleteSpace α
f : Filter α
inst✝ : f.NeBot
hf : f.TotallyBounded
m : Ultrafilter α := Ultrafilter.of f
⊢ ∃ x, ClusterPt x f

Tactic:
have hmf : m ≤ f := Ultrafilter.of_le f

Goal state after:
α : Type u
uniformSpace : UniformSpace α
inst✝¹ : CompleteSpace α
f : Filter α
inst✝ : f.NeBot
hf : f.TotallyBounded
m : Ultrafilter α := Ultrafilter.of f
hmf : ↑m ≤ f
⊢ ∃ x, ClusterPt x f
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
x : α
p : Filter ι
hp : p.NeBot
hf : UniformCauchySeqOn F p s
hx : x ∈ s
⊢ Cauchy (map (fun i ↦ F i x) p)

Tactic:
by
  simp only [cauchy_map_iff, hp, true_and]
  intro u hu
  rw [mem_map]
  filter_upwards [hf u hu] with p hp using hp x hx

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
⊢ IsComplete (range f) ↔ CompleteSpace β

Tactic:
hsurj.range_eq,

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : IsUniformInducing f
hsurj : Surjective f
⊢ IsComplete univ ↔ CompleteSpace β
Module: Mathlib.Algebra.Order.Group.MinMax

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ min (a / b) (a / c) = a / max b c

Tactic:
simp only [div_eq_mul_inv, min_mul_mul_left, min_inv_inv']

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 α
l : Filter ι
inst✝ : l.NeBot
F : ι → X → α
f : X → α
x₀ : X
h₁ : ∀ (x : X), Tendsto (fun i ↦ F i x) l (𝓝 (f x))
h₂ : EquicontinuousWithinAt F univ x₀
⊢ ContinuousWithinAt f univ x₀

Tactic:
exact continuousWithinAt_of_equicontinuousWithinAt (fun x _ ↦ h₁ x) (h₁ x₀) h₂

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

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
n : ℕ
hn : n ≠ 0
⊢ ⊥ * ⊥ ^ (n - 1) = ⊥

Tactic:
bot_mul

Goal state after:
α : Type u_2
inst✝ : Monoid α
n : ℕ
hn : n ≠ 0
⊢ ⊥ = ⊥
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: Γ : Type u_4
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : SMul Γ T
inst✝³ : ProperlyDiscontinuousSMul Γ T
inst✝² : T2Space T
inst✝¹ : LocallyCompactSpace T
inst✝ : ContinuousConstSMul Γ T
x : T
⊢ ∃ U ∈ 𝓝 x, ∀ (γ : Γ), γ • x ≠ x → Disjoint ((fun x ↦ γ • x) '' U) U

Tactic:
by
  convert! exists_nhds_image_smul_eq_self Γ x using 4
  rw [← not_imp_not]
  simp [Set.not_disjoint_iff_nonempty_inter]

Goal state after: