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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LocallyConnectedSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsCoinducing f
⊢ LocallyConnectedSpace β

Tactic:
by
  refine locallyConnectedSpace_iff_connectedComponentIn_open.2 fun F hF y _ ↦ ?_
  rw [← hf.isOpen_preimage, hf.continuous.continuousOn.preimage_connectedComponentIn]
  exact isOpen_biUnion fun x _ ↦ (hF.preimage hf.continuous).connectedComponentIn

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}

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:
Module: Mathlib.Topology.Connected.LocallyConnected

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

Tactic:
rcases isEmpty_or_nonempty (∀ i, X i) with he | hne
    · exact .inl he
    obtain ⟨x⟩ := hne
    classical
    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
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : f '' s ⊆ u ∪ v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
⊢ (f '' s ∩ (u ∩ v)).Nonempty

Tactic:
rcases continuousOn_iff'.1 hf v hv with ⟨v', hv', v'_eq⟩

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

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
contrapose! huv

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
huv : ¬s ⊆ u ∧ ¬s ⊆ v
⊢ (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
contrapose! huv

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
huv : ¬s ⊆ u ∧ ¬s ⊆ v
⊢ (s ∩ (u ∩ v)).Nonempty
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ᶜ
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
⊢ Disjoint (⋂ i, t i) s

Tactic:
apply Disjoint.symm

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 := ⋯
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
⊢ Disjoint s (⋂ i, t i)
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case inr
X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed[inst✝²] s
t_cl : IsClosed[inst✝²] t
st_dis : Disjoint s t
nonempty_X : Nonempty X
u : X → Set X
u_open : ∀ (a : X), IsOpen[inst✝²] (u a)
u_dis : ∀ (a : X), Disjoint (closure[inst✝²] (u a)) t
u_nhds : ∀ a ∈ s, a ∈ u a
f : ℕ → X
f_cov : s ⊆ ⋃ n, u (f n)
⊢ _root_.HasSeparatingCover s t

Tactic:
exact ⟨u ∘ f, f_cov, fun n ↦ ⟨u_open (f n), u_dis (f n)⟩⟩

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

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✝¹ : PreconnectedSpace α
inst✝ : PreconnectedSpace β
⊢ IsPreconnected univ

Tactic:
← univ_prod_univ

Goal state after:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝³ : TopologicalSpace α
s t u v : Set α
inst✝² : TopologicalSpace β
inst✝¹ : PreconnectedSpace α
inst✝ : PreconnectedSpace β
⊢ IsPreconnected (univ ×ˢ univ)
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
⊢ IsPreconnected univ

Tactic:
← IsInducing.subtypeVal.isPreconnected_image,

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
⊢ IsPreconnected (val '' univ)
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
inst✝ : T2Space β
di : IsDenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : s ∈ 𝓝 x
this : i '' s ∈ 𝓝 (i x)
⊢ False

Tactic:
rcases hd.inter_nhds_nonempty this with ⟨y, hyi, hys⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
inst✝ : T2Space β
di : IsDenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : s ∈ 𝓝 x
this : i '' s ∈ 𝓝 (i x)
y : β
hyi : y ∈ (range i)ᶜ
hys : y ∈ i '' s
⊢ False
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
inst✝ : TopologicalSpace γ
di : IsDenseInducing i
f : α → γ
a : α
hf : ContinuousAt f a
⊢ Tendsto f (𝓝 a) (𝓝 (di.extend f (i a)))

Tactic:
by
  rw [IsDenseInducing.extend, ← di.nhds_eq_comap]
  exact tendsto_nhds_limUnder ⟨_, hf⟩

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

Goal state before:
pp: α : Type u
β : Type v
ι✝ : Type u_1
X : ι✝ → Type u_2
inst✝ : TopologicalSpace α
s t u v : Set α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : ⋃ i, U i = univ
hconn : ∀ (i : ι), IsPreconnected (U i)
x : α
i : ι
hx : x ∈ U i
⊢ Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponent x

Tactic:
← connectedComponentIn_eq_image hx,

Goal state after:
α : Type u
β : Type v
ι✝ : Type u_1
X : ι✝ → Type u_2
inst✝ : TopologicalSpace α
s t u v : Set α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : ⋃ i, U i = univ
hconn : ∀ (i : ι), IsPreconnected (U i)
x : α
i : ι
hx : x ∈ U i
⊢ connectedComponentIn (U i) x = connectedComponent x
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
T : Set (Set X)
s : Set X
hs : IsGδ s
hd : Dense s
hc : T.Countable
hc' : ∀ t ∈ T, IsClosed[inst✝¹] t
hU : s ⊆ ⋃₀ T
⊢ s ⊆ ⋃ i ∈ T, i

Tactic:
rwa [← sUnion_eq_biUnion]

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

Goal state before:
pp: X : Type u_2
inst✝ : UniformSpace X
⊢ inst✝ = ⊥ ↔ uniformity X = 𝓟 SetRel.id

Tactic:
UniformSpace.ext_iff,

Goal state after:
X : Type u_2
inst✝ : UniformSpace X
⊢ (∀ (s : Set (X × X)), s ∈ uniformity X ↔ s ∈ uniformity X) ↔ uniformity X = 𝓟 SetRel.id
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
R : SetRel α α
f g : Filter α
inst✝ : R.IsSymm
⊢ R ∈ f ×ˢ g ↔ R ∈ g ×ˢ f

Tactic:
← R.inv_eq_self,

Goal state after:
α : Type ua
R : SetRel α α
f g : Filter α
inst✝ : R.IsSymm
⊢ R.inv ∈ f ×ˢ g ↔ R.inv ∈ g ×ˢ f
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
l : Filter α
h : Cauchy l
⊢ Cauchy ↑(Ultrafilter.of l)

Tactic:
by
  have := h.1
  have := Ultrafilter.of_le l
  exact ⟨Ultrafilter.neBot _, (Filter.prod_mono this this).trans h.2⟩

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
V : SetRel α α
h : V ∈ 𝓤 α
⊢ V.inv ∈ (𝓤 α).sets

Tactic:
rw [← comap_swap_uniformity]

Goal state after:
α : Type ua
inst✝ : UniformSpace α
V : SetRel α α
h : V ∈ 𝓤 α
⊢ V.inv ∈ (comap Prod.swap (𝓤 α)).sets
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ interior s ∈ (𝓤 α).lift' interior

Tactic:
exact mem_lift' hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
p' : Filter ι'
h : TendstoUniformlyOn F f p univ
h' : TendstoUniformlyOn F' f' p' univ
⊢ TendstoUniformlyOn (fun i ↦ Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') univ

Tactic:
← univ_prod_univ

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
p' : Filter ι'
h : TendstoUniformlyOn F f p univ
h' : TendstoUniformlyOn F' f' p' univ
⊢ TendstoUniformlyOn (fun i ↦ Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') (univ ×ˢ univ)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
s : α
x✝ : TopologicalSpace α := ⊥
⊢ 𝓝 s = comap (Prod.mk s) (𝓟 SetRel.id)

Tactic:
have := discreteTopology_bot α

Goal state after:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
s : α
x✝ : TopologicalSpace α := ⊥
this : DiscreteTopology α
⊢ 𝓝 s = comap (Prod.mk s) (𝓟 SetRel.id)
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst✝¹.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst✝¹.toTopologicalSpace] t)
S : Bool → Set α := fun b ↦ Bool.casesOn b s t
U : (b : Bool) → ↑(S b) → ι
hU : ∀ (b : Bool) (x : ↑(S b)), Disjoint (ball (↑x) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ x, ball (↑x) (B (U b x)) ∈ 𝓝ˢ (S b)
b : Bool
x : ↑(S b)
y : ↑(S !b)
hxy : U b x ≤ U (!b) y
⊢ ball (↑x) (B (U b x)) ∩ ball (↑y) (B (U (!b) y)) ⊆ ∅

Tactic:
intro z hz

Goal state after:
α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst✝¹.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst✝¹.toTopologicalSpace] t)
S : Bool → Set α := fun b ↦ Bool.casesOn b s t
U : (b : Bool) → ↑(S b) → ι
hU : ∀ (b : Bool) (x : ↑(S b)), Disjoint (ball (↑x) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ x, ball (↑x) (B (U b x)) ∈ 𝓝ˢ (S b)
b : Bool
x : ↑(S b)
y : ↑(S !b)
hxy : U b x ≤ U (!b) y
z : α
hz : z ∈ ball (↑x) (B (U b x)) ∩ ball (↑y) (B (U (!b) y))
⊢ z ∈ ∅
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s t : Set α
⊢ TotallyBounded (s ∪ t) ↔ TotallyBounded s ∧ TotallyBounded t

Tactic:
by
  rw [union_eq_iUnion, totallyBounded_iUnion]
  simp [and_comm]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ comap (fun x ↦ (f x.1, f x.2)) (𝓤 β) = 𝓤 α ↔ UniformSpace.comap f inst✝ = inst✝¹

Tactic:
UniformSpace.ext_iff,

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ comap (fun x ↦ (f x.1, f x.2)) (𝓤 β) = 𝓤 α ↔ ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ s ∈ 𝓤 α
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha : ua ∈ uas
hb : ub ∈ ubs
hf : UniformContinuous fun p ↦ f p.1 p.2
⊢ UniformContinuous fun p ↦ f p.1 p.2

Tactic:
by
  -- proof essentially copied from `continuous_sInf_dom`
  have ha := uniformContinuous_sInf_dom ha uniformContinuous_id
  have hb := uniformContinuous_sInf_dom hb uniformContinuous_id
  have h_unif_cont_id := @UniformContinuous.prodMap _ _ _ _ (sInf uas) (sInf ubs) ua ub _ _ ha hb
  exact @UniformContinuous.comp _ _ _ (id _) (id _) _ _ _ hf h_unif_cont_id

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
S : Set α
hg : IsUniformInducing g
⊢ UniformContinuousOn f S ↔ UniformContinuousOn (g ∘ f) S

Tactic:
dsimp only [UniformContinuousOn, Tendsto]
  rw [← hg.comap_uniformity, ← map_le_iff_le_comap, Filter.map_map, comp_def, comp_def]

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

Goal state before:
pp: β : Type v
inst✝ : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y ↦ (f x, f y) ∉ s
x✝ : UniformSpace α := ⊥
⊢ IsUniformEmbedding f

Tactic:
have := discreteTopology_bot α

Goal state after:
β : Type v
inst✝ : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y ↦ (f x, f y) ∉ s
x✝ : UniformSpace α := ⊥
this : DiscreteTopology α
⊢ IsUniformEmbedding f
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: β : Type v
inst✝³ : UniformSpace β
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : DiscreteTopology α
inst✝ : T0Space β
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y ↦ (f x, f y) ∉ s
⊢ IsClosedEmbedding f

Tactic:
by
  rcases @DiscreteTopology.eq_bot α _ _ with rfl; let _ : UniformSpace α := ⊥
  exact
    { (isUniformEmbedding_of_spaced_out hs hf).isEmbedding with
      isClosed_range := isClosed_range_of_spaced_out hs hf }

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

Goal state before:
pp: X : Type u_1
α : Type u_2
inst✝¹ : One α
inst✝ : TopologicalSpace X
⊢ closure[inst✝] ∅ = ∅

Tactic:
closure_empty

Goal state after:
X : Type u_1
α : Type u_2
inst✝¹ : One α
inst✝ : TopologicalSpace X
⊢ ∅ = ∅
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
x : α
⊢ UniformContinuous (Function.eval x ∘ ⇑toFun)

Tactic:
by
  change _ ≤ _
  rw [map_le_iff_le_comap,
    (UniformFun.hasBasis_uniformity α β).le_basis_iff ((𝓤 _).basis_sets.comap _)]
  exact fun U hU => ⟨U, hU, fun uv huv => huv x⟩

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

Goal state before:
pp: case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ UniformSpace.comap (Prod.fst ∘ ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ)) (uniformSpace α β) ⊓
      UniformSpace.comap (⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ))
        (UniformSpace.comap Prod.snd (uniformSpace α γ)) =
    uniformSpace α (β × γ)

Tactic:
← UniformSpace.comap_comap

Goal state after:
case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ UniformSpace.comap (Prod.fst ∘ ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ)) (uniformSpace α β) ⊓
      UniformSpace.comap (Prod.snd ∘ ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ)) (uniformSpace α γ) =
    uniformSpace α (β × γ)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
inst✝ : TopologicalSpace α
⊢ IsClosed[topologicalSpace α β] {f | Continuous[inst✝, inst✝¹.toTopologicalSpace] (toFun f)}

Tactic:
refine isClosed_iff_forall_filter.2 fun f u _ hu huf ↦ ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
inst✝ : TopologicalSpace α
f : α →ᵤ β
u : Filter (α →ᵤ β)
x✝ : u.NeBot
hu : u ≤ 𝓟 {f | Continuous[inst✝, inst✝¹.toTopologicalSpace] (toFun f)}
huf : u ≤ 𝓝 f
⊢ f ∈ {f | Continuous[inst✝, inst✝¹.toTopologicalSpace] (toFun f)}
Module: Mathlib.Order.Filter.AtTopBot.Map

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
⊢ map (⇑e) atTop = atTop

Tactic:
← e.comap_atTop,

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
⊢ map (⇑e) (comap (⇑e) atTop) = atTop
Module: Mathlib.Order.Filter.AtTopBot.Map

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
l : Filter γ
f : γ → α
e : α ≃o β
⊢ Tendsto (fun x ↦ e (f x)) l atTop ↔ Tendsto f l atTop

Tactic:
← e.comap_atTop,

Goal state after:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
l : Filter γ
f : γ → α
e : α ≃o β
⊢ Tendsto (fun x ↦ e (f x)) l atTop ↔ Tendsto f l (comap (⇑e) atTop)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
⊢ ⨅ i ∈ 𝔖,
      ⨅ i_1,
        ⨅ (_ : p i_1),
          𝓟
            (Prod.map (⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔖))
                (⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔖)) ⁻¹'
              UniformFun.gen (↑i) β (V i_1)) =
    ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i))

Tactic:
UniformFun.gen,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
⊢ ⨅ i ∈ 𝔖,
      ⨅ i_1,
        ⨅ (_ : p i_1),
          𝓟
            (Prod.map (⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔖))
                (⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔖)) ⁻¹'
              {uv | ∀ (x : ↑i), (UniformFun.toFun uv.1 x, UniformFun.toFun uv.2 x) ∈ V i_1}) =
    ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i))
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ a / x) ⁻¹' Icc b c = Icc (a / c) (a / b)

Tactic:
by
  simp [← Ici_inter_Iic, inter_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
⊢ IsUniformInducing
    ⇑((ofFun 𝔖).symm.trans
        ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))

Tactic:
constructor
      rw [uniformity_prod, comap_inf, comap_comap, comap_comap]
      have H := @UniformOnFun.inf_eq α (β × γ) 𝔖
        (UniformSpace.comap Prod.fst ‹_›) (UniformSpace.comap Prod.snd ‹_›)
      apply_fun (fun u ↦ @uniformity (α →ᵤ[𝔖] β × γ) u) at H
      convert! H.symm using 1
      rw [UniformOnFun.comap_eq, UniformOnFun.comap_eq]
      erw [inf_uniformity]
      rw [uniformity_comap, uniformity_comap]
      rfl

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

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
⊢ ⊤ * f = ⊤

Tactic:
by
  refine top_le_iff.1 fun s => ?_
  simp only [mem_mul, mem_top, exists_eq_left]
  rintro ⟨t, ht, hs⟩
  rwa [univ_mul_of_one_mem (mem_one.1 <| hf ht), univ_subset_iff] at hs

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
⊢ (fun x ↦ a * x + b) '' Ico c d = Ico (a * c + b) (a * d + b)

Tactic:
suffices (· + b) '' (a * ·) '' Ico c d = Ico (a * c + b) (a * d + b) by
    rwa [Set.image_image] at this

Goal state after:
K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
⊢ (fun x ↦ x + b) '' (fun x ↦ a * x) '' Ico c d = Ico (a * c + b) (a * d + b)